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 173 imim21b 382 pm3.48 878 jcab 907 nic-ax 1598 nic-axALT 1599 tbw-bijust 1623 merco1 1638 sbimi 1886 19.24 1900 19.23v 1902 2eu6 2558 axi5r 2594 r19.36v 3085 ceqsalt 3228 vtoclgft 3254 vtoclgftOLD 3255 spcgft 3285 mo2icl 3385 euind 3393 reu6 3395 reuind 3411 sbciegft 3466 elpwunsn 4224 dfiin2g 4553 invdisj 4638 ssrel 5207 dff3 6372 fnoprabg 6761 tfindsg 7060 findsg 7093 zfrep6 7134 tz7.48-1 7538 odi 7659 r1sdom 8637 kmlem6 8977 kmlem12 8983 zorng 9326 squeeze0 10926 xrsupexmnf 12135 xrinfmexpnf 12136 mptnn0fsuppd 12798 reuccats1lem 13479 rexanre 14086 pmatcollpw2lem 20582 tgcnp 21057 lmcvg 21066 iblcnlem 23555 limcresi 23649 isch3 28098 disjexc 29406 cntmeas 30289 bnj900 30999 bnj1172 31069 bnj1174 31071 bnj1176 31073 axextdfeq 31703 hbimtg 31712 nn0prpw 32318 meran3 32412 waj-ax 32413 lukshef-ax2 32414 imsym1 32417 bj-orim2 32541 bj-currypeirce 32544 bj-andnotim 32573 bj-ssbequ2 32643 bj-ssbid2ALT 32646 bj-19.21bit 32680 bj-ceqsalt0 32873 bj-ceqsalt1 32874 wl-embant 33293 contrd 33899 ax12indi 34229 ltrnnid 35422 ismrc 37264 rp-fakenanass 37860 frege55lem1a 38160 frege55lem1b 38189 frege55lem1c 38210 frege92 38249 pm11.71 38597 exbir 38684 ax6e2ndeqVD 39145 ax6e2ndeqALT 39167 r19.36vf 39324 nn0sumshdiglemA 42413 nn0sumshdiglemB 42414 |
Copyright terms: Public domain | W3C validator |