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  2591  ceqsalg  2787  rcla4t  2852  elabgt  2886  tfi  4616  fvmptt  5549  fnfi  7102  finsschain  7130  ordiso2  7198  ordtypelem7  7207  dfom3  7316  infdiffi  7326  cantnfp1lem3  7350  cantnf  7363  r1ordg  7418  ttukeylem6  8109  fpwwe2lem8  8227  wunfi  8311  dfnn2  9727  pgpfac1  15277  fiuncmp  17093  filssufilg  17568  ufileu  17576  pjnormssi  22708  waj-ax  24228  wl-mps  24278  psgnunilem3  26786  atbiffatnnb  27170  bnj1110  28061  ax12olem18K  28232  ax12olem18X  28233  ax10lem24X  28260  a12study4  28284  ax10lem17ALT  28290  a12study10  28303  a12study10n  28304  ax9lem17  28323
This theorem was proved from axioms:  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator