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

Theorem a2i 14
Description: Inference derived from axiom ax-2 8. (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 8 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  ->  ps )  ->  ( ph  ->  ch ) ) )
31, 2ax-mp 10 1  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  imim2i  15  mpd  16  sylcom  27  pm2.43  49  pm2.18  104  ancl  531  ancr  534  anc2r  541  ax12olem18  1652  ax10lem24  1673  nfim1  1805  hbim1  1810  ralimia  2578  ceqsalg  2750  rcla4t  2814  elabgt  2848  tfi  4535  fvmptt  5467  fnfi  7019  finsschain  7046  ordiso2  7114  ordtypelem7  7123  dfom3  7232  infdiffi  7242  cantnfp1lem3  7266  cantnf  7279  r1ordg  7334  ttukeylem6  8025  fpwwe2lem8  8139  wunfi  8223  dfnn2  9639  pgpfac1  15150  fiuncmp  16963  filssufilg  17438  ufileu  17446  pjnormssi  22578  waj-ax  24027  wl-mps  24077  psgnunilem3  26585  atbiffatnnb  26866  bnj1110  27701  a12study4  27806  ax10lem17ALT  27812  a12study10  27825  a12study10n  27826  ax9lem17  27845
This theorem was proved from axioms:  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator