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, 29-Dec-1992.)
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 setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-2 7
This theorem is referenced by:  imim2i  14  mpd  15  sylcom  29  pm2.43  51  pm2.18  110  ancl  546  ancr  549  anc2r  556  hbim1  1856  ralimia  2817  ceqsalgALT  3104  rspct  3172  elabgt  3210  fvmptt  5901  tfi  6577  fnfi  7703  finsschain  7732  ordiso2  7843  ordtypelem7  7852  dfom3  7967  infdiffi  7977  cantnfp1lem3  8002  cantnf  8015  cantnfp1lem3OLD  8028  cantnfOLD  8037  r1ordg  8099  ttukeylem6  8797  fpwwe2lem8  8918  wunfi  9002  dfnn2  10449  psgnunilem3  16124  pgpfac1  16706  fiuncmp  19142  filssufilg  19619  ufileu  19627  pjnormssi  25744  waj-ax  28424  wl-mps  28516  atbiffatnnb  30095  bnj1110  32325  bj-equsal1  32684  bj-equsal2  32685
  Copyright terms: Public domain W3C validator