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  1535  equidqe  1554  equid  1723  ax10  1739  hbae  1740  vtoclgaf  2837  vtocl2gaf  2839  vtocl3gaf  2841  ifmdc  3611  elinti  3893  copsexg  4287  nlimsucg  4613  tfisi  4634  vtoclr  4722  issref  5064  relresfld  5211  f1o2ndf1  6313  tfrlem9  6404  nndi  6571  mulcanpig  7447  lediv2a  8967  seq3id3  10667  resqrexlemdecn  11265  ndvdssub  12183  bitsinv1  12215  nn0seqcvgd  12305  modprm0  12519  mplbasss  14400  fiinopn  14418  xmetunirn  14772  mopnval  14856  plyssc  15153  2lgsoddprm  15532  ax1hfs  15946