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  1732  nfim1  1821  dvelimv  1879  ralimia  2616  ceqsalg  2812  rspct  2877  elabgt  2911  tfi  4644  fvmptt  5615  fnfi  7134  finsschain  7162  ordiso2  7230  ordtypelem7  7239  dfom3  7348  infdiffi  7358  cantnfp1lem3  7382  cantnf  7395  r1ordg  7450  ttukeylem6  8141  fpwwe2lem8  8259  wunfi  8343  dfnn2  9759  pgpfac1  15315  fiuncmp  17131  filssufilg  17606  ufileu  17614  pjnormssi  22748  waj-ax  24853  wl-mps  24903  psgnunilem3  27419  atbiffatnnb  27881  bnj1110  29012  a12study4  29117  ax10lem17ALT  29123  a12study10  29136  a12study10n  29137  ax9lem17  29156
This theorem was proved from axioms:  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator