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  1825  nfim1OLD  1827  dvelimvOLD  1994  ralimia  2739  ceqsalg  2940  rspct  3005  elabgt  3039  tfi  4792  fvmptt  5779  fnfi  7343  finsschain  7371  ordiso2  7440  ordtypelem7  7449  dfom3  7558  infdiffi  7568  cantnfp1lem3  7592  cantnf  7605  r1ordg  7660  ttukeylem6  8350  fpwwe2lem8  8468  wunfi  8552  dfnn2  9969  pgpfac1  15593  fiuncmp  17421  filssufilg  17896  ufileu  17904  pjnormssi  23624  waj-ax  26068  wl-mps  26118  psgnunilem3  27287  atbiffatnnb  27748  bnj1110  29057  dvelimvNEW7  29168  equsalihAUX7  29194
This theorem was proved from axioms:  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator