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  1819  nfim1OLD  1821  dvelimvOLD  1985  ralimia  2722  ceqsalg  2923  rspct  2988  elabgt  3022  tfi  4773  fvmptt  5759  fnfi  7320  finsschain  7348  ordiso2  7417  ordtypelem7  7426  dfom3  7535  infdiffi  7545  cantnfp1lem3  7569  cantnf  7582  r1ordg  7637  ttukeylem6  8327  fpwwe2lem8  8445  wunfi  8529  dfnn2  9945  pgpfac1  15565  fiuncmp  17389  filssufilg  17864  ufileu  17872  pjnormssi  23519  waj-ax  25878  wl-mps  25928  psgnunilem3  27088  atbiffatnnb  27549  bnj1110  28689  dvelimvNEW7  28800  equsalihAUX7  28826
This theorem was proved from axioms:  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator