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  2880  vtocl2gaf  2882  vtocl3gaf  2884  ifmdc  3665  elinti  3958  copsexg  4360  nlimsucg  4688  tfisi  4709  vtoclr  4798  ssrelrn  4947  issref  5145  relresfld  5292  f1o2ndf1  6424  tfrlem9  6550  nndi  6719  mulcanpig  7650  lediv2a  9169  seq3id3  10886  resqrexlemdecn  11697  ndvdssub  12616  bitsinv1  12648  nn0seqcvgd  12738  modprm0  12952  mplbasss  14851  fiinopn  14869  xmetunirn  15223  mopnval  15307  plyssc  15604  2lgsoddprm  15986  uspgrushgr  16175  uspgrupgr  16176  usgruspgr  16178  usgredg2vlem2  16218  ax1hfs  16871