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  394  pm2.13dc  870  hbequid  1493  equidqe  1512  equid  1677  ax10  1695  hbae  1696  vtoclgaf  2746  vtocl2gaf  2748  vtocl3gaf  2750  ifmdc  3504  elinti  3775  copsexg  4161  nlimsucg  4476  tfisi  4496  vtoclr  4582  issref  4916  relresfld  5063  f1o2ndf1  6118  tfrlem9  6209  nndi  6375  mulcanpig  7136  lediv2a  8646  seq3id3  10273  resqrexlemdecn  10777  ndvdssub  11616  nn0seqcvgd  11711  fiinopn  12160  xmetunirn  12516  mopnval  12600  ax1hfs  13229