MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a2i Structured version   Unicode version

Theorem a2i 13
Description: Inference derived from axiom ax-2 7. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
a2i.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
a2i  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)

Proof of Theorem a2i
StepHypRef Expression
1 a2i.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 ax-2 7 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  ->  ps )  ->  ( ph  ->  ch ) ) )
31, 2ax-mp 5 1  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim2i  14  mpd  15  sylcom  28  pm2.43  50  pm2.18  105  ancl  531  ancr  534  anc2r  541  hbim1  1831  nfim1OLD  1833  dvelimvOLD  2031  ralimia  2785  ceqsalg  2986  rspct  3051  elabgt  3085  tfi  4862  fvmptt  5849  fnfi  7413  finsschain  7442  ordiso2  7513  ordtypelem7  7522  dfom3  7631  infdiffi  7641  cantnfp1lem3  7665  cantnf  7678  r1ordg  7733  ttukeylem6  8425  fpwwe2lem8  8543  wunfi  8627  dfnn2  10044  pgpfac1  15669  fiuncmp  17498  filssufilg  17974  ufileu  17982  pjnormssi  23702  waj-ax  26195  wl-mps  26245  psgnunilem3  27434  atbiffatnnb  27895  bnj1110  29449  dvelimvNEW7  29560  equsalihAUX7  29586
This theorem was proved from axioms:  ax-mp 5  ax-2 7
  Copyright terms: Public domain W3C validator