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

Theorem a2i 12
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  13  mpd  14  sylcom  25  pm2.43  47  pm2.18  102  ancl  529  ancr  532  anc2r  539  hbim1  1744  nfim1  1833  dvelimv  1892  ralimia  2629  ceqsalg  2825  rspct  2890  elabgt  2924  tfi  4660  fvmptt  5631  fnfi  7150  finsschain  7178  ordiso2  7246  ordtypelem7  7255  dfom3  7364  infdiffi  7374  cantnfp1lem3  7398  cantnf  7411  r1ordg  7466  ttukeylem6  8157  fpwwe2lem8  8275  wunfi  8359  dfnn2  9775  pgpfac1  15331  fiuncmp  17147  filssufilg  17622  ufileu  17630  pjnormssi  22764  waj-ax  24925  wl-mps  24975  psgnunilem3  27522  atbiffatnnb  27984  bnj1110  29328  dvelimvNEW7  29439  equsalihAUX7  29465  a12study4  29739  ax10lem17ALT  29745  a12study10  29758  a12study10n  29759  ax9lem17  29778
This theorem was proved from axioms:  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator