![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > a2i | Unicode version |
Description: Inference derived from axiom ax-2 7. (Contributed by NM, 29-Dec-1992.) |
Ref | Expression |
---|---|
a2i.1 |
Ref | Expression |
---|---|
a2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a2i.1 | . 2 | |
2 | ax-2 7 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 |
This theorem is referenced by: imim2i 14 mpd 15 sylcom 29 pm2.43 51 pm2.18 110 ancl 546 ancr 549 anc2r 556 hbim1 1918 ralimia 2848 ceqsalgALT 3135 rspct 3203 elabgt 3243 fvmptt 5971 tfi 6688 fnfi 7818 finsschain 7847 ordiso2 7961 ordtypelem7 7970 dfom3 8085 infdiffi 8095 cantnfp1lem3 8120 cantnf 8133 cantnfp1lem3OLD 8146 cantnfOLD 8155 r1ordg 8217 ttukeylem6 8915 fpwwe2lem8 9036 wunfi 9120 dfnn2 10574 psgnunilem3 16521 pgpfac1 17131 fiuncmp 19904 filssufilg 20412 ufileu 20420 pjnormssi 27087 waj-ax 29879 wl-mps 29971 atbiffatnnb 32108 bnj1110 34038 bj-equsal1 34397 bj-equsal2 34398 |
This theorem was proved from axioms: ax-mp 5 ax-2 7 |
Copyright terms: Public domain | W3C validator |