Theorem pm2.43i 49

Description: Inference absorbing redundant antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)

Hypothesis

Ref	Expression
pm2.43i.1	|- ( ph -> ( ph -> ps ) )

Assertion

Ref	Expression
pm2.43i	|- ( ph -> ps )

Proof of Theorem pm2.43i

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ph -> ph )
2		pm2.43i.1	. 2 |- ( ph -> ( ph -> ps ) )
3	1, 2	mpd 13	1 |- ( ph -> ps )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  sylc  62  impbid  128  ibi  175  anidms  395  pm2.13dc  871  hbequid  1493  equidqe  1512  equid  1681  ax10  1697  hbae  1698  vtoclgaf  2777  vtocl2gaf  2779  vtocl3gaf  2781  ifmdc  3542  elinti  3816  copsexg  4203  nlimsucg  4523  tfisi  4544  vtoclr  4631  issref  4965  relresfld  5112  f1o2ndf1  6169  tfrlem9  6260  nndi  6426  mulcanpig  7238  lediv2a  8749  seq3id3  10388  resqrexlemdecn  10894  ndvdssub  11802  nn0seqcvgd  11898  fiinopn  12362  xmetunirn  12718  mopnval  12802  ax1hfs  13604