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

Theorem a2i 13
Description: Inference derived from axiom ax-2 6. (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 6 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  ->  ps )  ->  ( ph  ->  ch ) ) )
31, 2ax-mp 8 1  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim2i  14  mpd  15  sylcom  27  pm2.43  49  pm2.18  104  ancl  530  ancr  533  anc2r  540  hbim1  1829  nfim1OLD  1831  dvelimvOLD  2028  ralimia  2766  ceqsalg  2967  rspct  3032  elabgt  3066  tfi  4819  fvmptt  5806  fnfi  7370  finsschain  7399  ordiso2  7468  ordtypelem7  7477  dfom3  7586  infdiffi  7596  cantnfp1lem3  7620  cantnf  7633  r1ordg  7688  ttukeylem6  8378  fpwwe2lem8  8496  wunfi  8580  dfnn2  9997  pgpfac1  15621  fiuncmp  17450  filssufilg  17926  ufileu  17934  pjnormssi  23654  waj-ax  26107  wl-mps  26157  psgnunilem3  27329  atbiffatnnb  27790  bnj1110  29103  dvelimvNEW7  29214  equsalihAUX7  29240
This theorem was proved from axioms:  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator