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  1850  ralimia  2784  ceqsalgALT  2993  rspct  3061  elabgt  3098  fvmptt  5784  tfi  6459  fnfi  7581  finsschain  7610  ordiso2  7721  ordtypelem7  7730  dfom3  7845  infdiffi  7855  cantnfp1lem3  7880  cantnf  7893  cantnfp1lem3OLD  7906  cantnfOLD  7915  r1ordg  7977  ttukeylem6  8675  fpwwe2lem8  8796  wunfi  8880  dfnn2  10327  psgnunilem3  15993  pgpfac1  16569  fiuncmp  18982  filssufilg  19459  ufileu  19467  pjnormssi  25523  waj-ax  28212  wl-mps  28299  atbiffatnnb  29880  bnj1110  31860  bj-equsal1  32188  bj-equsal2  32189
  Copyright terms: Public domain W3C validator