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  887  hbequid  1537  equidqe  1556  equid  1725  ax10  1741  hbae  1742  vtoclgaf  2840  vtocl2gaf  2842  vtocl3gaf  2844  ifmdc  3617  elinti  3900  copsexg  4296  nlimsucg  4622  tfisi  4643  vtoclr  4731  ssrelrn  4878  issref  5074  relresfld  5221  f1o2ndf1  6327  tfrlem9  6418  nndi  6585  mulcanpig  7468  lediv2a  8988  seq3id3  10691  resqrexlemdecn  11398  ndvdssub  12316  bitsinv1  12348  nn0seqcvgd  12438  modprm0  12652  mplbasss  14533  fiinopn  14551  xmetunirn  14905  mopnval  14989  plyssc  15286  2lgsoddprm  15665  ax1hfs  16154