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  1527  equidqe  1546  equid  1715  ax10  1731  hbae  1732  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  ifmdc  3602  elinti  3884  copsexg  4278  nlimsucg  4603  tfisi  4624  vtoclr  4712  issref  5053  relresfld  5200  f1o2ndf1  6295  tfrlem9  6386  nndi  6553  mulcanpig  7421  lediv2a  8941  seq3id3  10635  resqrexlemdecn  11196  ndvdssub  12114  bitsinv1  12146  nn0seqcvgd  12236  modprm0  12450  mplbasss  14330  fiinopn  14348  xmetunirn  14702  mopnval  14786  plyssc  15083  2lgsoddprm  15462  ax1hfs  15831