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  4612  tfisi  4633  vtoclr  4721  issref  5062  relresfld  5209  f1o2ndf1  6304  tfrlem9  6395  nndi  6562  mulcanpig  7430  lediv2a  8950  seq3id3  10650  resqrexlemdecn  11242  ndvdssub  12160  bitsinv1  12192  nn0seqcvgd  12282  modprm0  12496  mplbasss  14376  fiinopn  14394  xmetunirn  14748  mopnval  14832  plyssc  15129  2lgsoddprm  15508  ax1hfs  15877