![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imim2i | Structured version Visualization version Unicode version |
Description: Inference adding common antecedents in an implication. Inference associated with imim2 55. 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: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: imim12i 59 imim3i 61 imim12 100 ja 165 imim21b 369 pm3.48 844 jcab 874 nic-ax 1556 nic-axALT 1557 tbw-bijust 1581 merco1 1596 sbimi 1803 19.24 1816 19.23v 1818 2eu6 2387 axi5r 2423 r19.36v 2938 ceqsalt 3070 vtoclgft 3096 spcgft 3126 mo2icl 3217 euind 3225 reu6 3227 reuind 3243 sbciegft 3298 elpwunsn 4012 dfiin2g 4311 invdisj 4391 dff3 6035 fnoprabg 6397 tfindsg 6687 findsg 6720 zfrep6 6761 tz7.48-1 7160 odi 7280 r1sdom 8245 kmlem6 8585 kmlem12 8591 zorng 8934 squeeze0 10509 xrsupexmnf 11590 xrinfmexpnf 11591 mptnn0fsuppd 12210 reuccats1lem 12836 rexanre 13409 pmatcollpw2lem 19801 tgcnp 20269 lmcvg 20278 iblcnlem 22746 limcresi 22840 isch3 26894 disjexc 28203 cntmeas 29048 bnj900 29740 bnj1172 29810 bnj1174 29812 bnj1176 29814 axextdfeq 30444 hbimtg 30453 nn0prpw 30979 meran3 31073 waj-ax 31074 lukshef-ax2 31075 imsym1 31078 bj-andnotim 31172 bj-ssbequ2 31256 bj-ssbid2ALT 31259 bj-19.21bit 31283 bj-ceqsalt0 31482 bj-ceqsalt1 31483 wl-embantALT 31847 contrd 32333 ax12indi 32515 ltrnnid 33701 ismrc 35543 rp-fakenanass 36159 frege55lem1a 36462 frege55lem1b 36491 frege55lem1c 36512 frege92 36551 pm11.71 36747 exbir 36833 ax6e2ndeqVD 37306 ax6e2ndeqALT 37328 nn0sumshdiglemA 40483 nn0sumshdiglemB 40484 |
Copyright terms: Public domain | W3C validator |