imim2i - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imim2i		Structured version Visualization version GIF version

Theorem imim2i 16

Description: Inference adding common antecedents in an implication. Inference associated with imim2 58. Its associated inference is syl 17. (Contributed by NM, 28-Dec-1992.)

**Hypothesis**
Ref	Expression
imim2i.1	⊢ (𝜑 → 𝜓)

**Assertion**
Ref	Expression
imim2i	⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

**Proof of Theorem imim2i**
Step	Hyp	Ref	Expression
1		imim2i.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
3	2	a2i 14	1 ⊢ ((𝜒 → 𝜑) → (𝜒 → 𝜓))

Colors of variables: wff setvar class

Syntax hints: → wi 4

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7

This theorem is referenced by: imim12i 62 imim3i 64 ja 186 imim21b 394 jcab 517 pm3.48 962 nanass 1504 nic-ax 1668 nic-axALT 1669 tbw-bijust 1693 merco1 1708 19.23v 1938 19.24 1982 hbsbwOLD 2162 sb4a 2475 2eu6 2648 axi5r 2691 ralrexbidOLD 3104 r19.36v 3180 ceqsal1t 3502 vtoclgft 3538 spcgft 3575 elabgt 3660 elabgtOLD 3661 mo2icl 3709 euind 3719 reu6 3721 reuind 3748 sbciegftOLD 3815 elpwunsn 4688 dfiin2g 5035 invdisj 5132 ssrel 5784 ssrelOLD 5785 dff3 7110 fnoprabg 7543 tfindsg 7865 findsg 7905 zfrep6 7958 tz7.48-1 8464 odi 8600 r1sdom 9798 kmlem6 10179 kmlem12 10185 zorng 10528 squeeze0 12148 xrsupexmnf 13317 xrinfmexpnf 13318 mptnn0fsuppd 13996 rexanre 15326 pmatcollpw2lem 22692 tgcnp 23170 lmcvg 23179 iblcnlem 25731 limcresi 25827 isch3 31064 disjexc 32396 cntmeas 33845 bnj900 34560 bnj1172 34632 bnj1174 34634 bnj1176 34636 gonarlem 35004 goalrlem 35006 axextdfeq 35393 hbimtg 35402 nn0prpw 35807 meran3 35897 waj-ax 35898 lukshef-ax2 35899 imsym1 35902 bj-peircestab 36028 bj-orim2 36031 bj-andnotim 36065 bj-ssbid2ALT 36139 bj-19.21bit 36167 bj-substax12 36198 bj-ceqsalt0 36362 bj-ceqsalt1 36363 wl-embant 36977 contrd 37570 ax12indi 38416 ltrnnid 39609 ismrc 42121 frege55lem1a 43296 frege55lem1b 43325 frege55lem1c 43346 frege92 43385 pm11.71 43834 exbir 43917 ax6e2ndeqVD 44348 ax6e2ndeqALT 44370 r19.36vf 44502 nn0sumshdiglemA 47692 nn0sumshdiglemB 47693 setrec2mpt 48128

W3C validator

	
		OSZAR »