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  1904  ralimia  2834  ceqsalgALT  3121  rspct  3189  elabgt  3229  fvmptt  5956  tfi  6673  fnfi  7800  finsschain  7829  ordiso2  7943  ordtypelem7  7952  dfom3  8067  infdiffi  8077  cantnfp1lem3  8102  cantnf  8115  cantnfp1lem3OLD  8128  cantnfOLD  8137  r1ordg  8199  ttukeylem6  8897  fpwwe2lem8  9018  wunfi  9102  dfnn2  10555  psgnunilem3  16395  pgpfac1  17005  fiuncmp  19777  filssufilg  20285  ufileu  20293  pjnormssi  26959  waj-ax  29854  wl-mps  29946  atbiffatnnb  31946  bnj1110  33771  bj-equsal1  34145  bj-equsal2  34146
  Copyright terms: Public domain W3C validator