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

Theorem a2i 14
Description: Inference distributing an antecedent. Inference associated with ax-2 7. Its associated inference is mpd 15. (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:  mpd  15  imim2i  16  sylcom  30  pm2.43  53  pm2.18  113  ancl  548  ancr  551  anc2r  558  hbim1  1974  ralimia  2816  ceqsalgALT  3107  rspct  3175  elabgt  3215  fvmptt  5978  tfi  6691  fnfi  7852  finsschain  7884  ordiso2  8033  ordtypelem7  8042  dfom3  8155  infdiffi  8165  cantnfp1lem3  8187  cantnf  8200  r1ordg  8251  ttukeylem6  8945  fpwwe2lem8  9063  wunfi  9147  dfnn2  10623  trclfvcotr  13062  psgnunilem3  17125  pgpfac1  17701  fiuncmp  20406  filssufilg  20913  ufileu  20921  pjnormssi  27807  bnj1110  29787  waj-ax  31067  bj-equsal1  31384  bj-equsal2  31385  wl-mps  31757  atbiffatnnb  38213
  Copyright terms: Public domain W3C validator