NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  a2i Unicode version

Theorem a2i 12
Description: Inference derived from axiom ax-2 7. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
a2i.1
Assertion
Ref Expression
a2i

Proof of Theorem a2i
StepHypRef Expression
1 a2i.1 . 2
2 ax-2 7 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:   wi 4
This theorem was proved from axioms:  ax-mp 5  ax-2 7
This theorem is referenced by:  imim2i  13  mpd  14  sylcom  25  pm2.43  47  pm2.18  102  ancl  529  ancr  532  anc2r  539  hbim1  1810  nfim1OLD  1812  dvelimv  1939  ralimia  2687  ceqsalg  2883  rspct  2948  elabgt  2982  peano2  4403  peano5  4409  spfininduct  4540  fvopab4t  5385
  Copyright terms: Public domain W3C validator