![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imim2i | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
imim2i.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
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 imim12 105 ja 175 imim21b 386 jcab 510 pm3.48 946 nanass 1486 nanassOLD 1487 nic-ax 1636 nic-axALT 1637 tbw-bijust 1661 merco1 1676 19.23v 1901 19.24 1942 sb4a 2429 sbimiOLD 2435 sbimiALT 2504 2eu6 2688 axi5r 2740 r19.36v 3283 ceqsalt 3448 vtoclgft 3474 spcgft 3506 mo2icl 3621 euind 3629 reu6 3631 reuind 3655 sbciegft 3714 elpwunsn 4496 dfiin2g 4828 invdisj 4916 ssrel 5508 dff3 6691 fnoprabg 7093 tfindsg 7393 findsg 7426 zfrep6 7470 tz7.48-1 7884 odi 8008 r1sdom 8999 kmlem6 9377 kmlem12 9383 zorng 9726 squeeze0 11346 xrsupexmnf 12517 xrinfmexpnf 12518 mptnn0fsuppd 13184 reuccats1lemOLD 13923 rexanre 14570 pmatcollpw2lem 21092 tgcnp 21568 lmcvg 21577 iblcnlem 24095 limcresi 24189 isch3 28800 disjexc 30112 cntmeas 31130 bnj900 31848 bnj1172 31918 bnj1174 31920 bnj1176 31922 axextdfeq 32563 hbimtg 32572 nn0prpw 33192 meran3 33281 waj-ax 33282 lukshef-ax2 33283 imsym1 33286 bj-orim2 33408 bj-andnotim 33439 bj-ssbid2ALT 33505 bj-19.21bit 33534 bj-ceqsalt0 33693 bj-ceqsalt1 33694 wl-embant 34191 contrd 34819 ax12indi 35525 ltrnnid 36717 ismrc 38693 frege55lem1a 39575 frege55lem1b 39604 frege55lem1c 39625 frege92 39664 pm11.71 40146 exbir 40231 ax6e2ndeqVD 40662 ax6e2ndeqALT 40684 r19.36vf 40827 nn0sumshdiglemA 44048 nn0sumshdiglemB 44049 |
Copyright terms: Public domain | W3C validator |