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  24264  wl-mps  24314  psgnunilem3  26831  atbiffatnnb  27293  bnj1110  28385  a12study4  28490  ax10lem17ALT  28496  a12study10  28509  a12study10n  28510  ax9lem17  28529
This theorem was proved from axioms:  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator