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

Theorem a2i 13
Description: Inference derived from axiom ax-2 7. (Contributed by NM, 29-Dec-1992.)
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 7 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  ->  ps )  ->  ( ph  ->  ch ) ) )
31, 2ax-mp 5 1  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-2 7
This theorem is referenced by:  imim2i  14  mpd  15  sylcom  29  pm2.43  51  pm2.18  110  ancl  546  ancr  549  anc2r  556  hbim1  1865  ralimia  2858  ceqsalgALT  3144  rspct  3212  elabgt  3252  fvmptt  5972  tfi  6683  fnfi  7810  finsschain  7839  ordiso2  7952  ordtypelem7  7961  dfom3  8076  infdiffi  8086  cantnfp1lem3  8111  cantnf  8124  cantnfp1lem3OLD  8137  cantnfOLD  8146  r1ordg  8208  ttukeylem6  8906  fpwwe2lem8  9027  wunfi  9111  dfnn2  10561  psgnunilem3  16394  pgpfac1  17003  fiuncmp  19772  filssufilg  20280  ufileu  20288  pjnormssi  26901  waj-ax  29797  wl-mps  29889  atbiffatnnb  31889  bnj1110  33473  bj-equsal1  33834  bj-equsal2  33835  bj-frege55lem1a  37231  frege55lem1b  37243
  Copyright terms: Public domain W3C validator