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  129  ibi  176  anidms  397  pm2.13dc  886  hbequid  1524  equidqe  1543  equid  1712  ax10  1728  hbae  1729  vtoclgaf  2825  vtocl2gaf  2827  vtocl3gaf  2829  ifmdc  3597  elinti  3879  copsexg  4273  nlimsucg  4598  tfisi  4619  vtoclr  4707  issref  5048  relresfld  5195  f1o2ndf1  6281  tfrlem9  6372  nndi  6539  mulcanpig  7395  lediv2a  8914  seq3id3  10595  resqrexlemdecn  11156  ndvdssub  12071  nn0seqcvgd  12179  modprm0  12392  fiinopn  14172  xmetunirn  14526  mopnval  14610  plyssc  14885  ax1hfs  15564