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  hbim1  1733  nfim1  1822  dvelimv  1880  ralimia  2617  ceqsalg  2813  rspct  2878  elabgt  2912  tfi  4643  fvmptt  5576  fnfi  7129  finsschain  7157  ordiso2  7225  ordtypelem7  7234  dfom3  7343  infdiffi  7353  cantnfp1lem3  7377  cantnf  7390  r1ordg  7445  ttukeylem6  8136  fpwwe2lem8  8254  wunfi  8338  dfnn2  9754  pgpfac1  15309  fiuncmp  17125  filssufilg  17600  ufileu  17608  pjnormssi  22740  waj-ax  24260  wl-mps  24310  psgnunilem3  26818  atbiffatnnb  27260  bnj1110  28279  a12study4  28384  ax10lem17ALT  28390  a12study10  28403  a12study10n  28404  ax9lem17  28423
This theorem was proved from axioms:  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator