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  893  hbequid  1562  equidqe  1581  equid  1749  ax10  1765  hbae  1766  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  ifmdc  3652  elinti  3942  copsexg  4342  nlimsucg  4670  tfisi  4691  vtoclr  4780  ssrelrn  4928  issref  5126  relresfld  5273  f1o2ndf1  6402  tfrlem9  6528  nndi  6697  mulcanpig  7598  lediv2a  9117  seq3id3  10832  resqrexlemdecn  11635  ndvdssub  12554  bitsinv1  12586  nn0seqcvgd  12676  modprm0  12890  mplbasss  14780  fiinopn  14798  xmetunirn  15152  mopnval  15236  plyssc  15533  2lgsoddprm  15915  uspgrushgr  16104  uspgrupgr  16105  usgruspgr  16107  usgredg2vlem2  16147  ax1hfs  16800