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  401  pm2.13dc  897  hbequid  1566  equidqe  1585  equid  1753  ax10  1769  hbae  1770  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  ifmdc  3680  elinti  3974  copsexg  4379  nlimsucg  4708  tfisi  4729  vtoclr  4818  ssrelrn  4967  issref  5165  relresfld  5312  f1o2ndf1  6454  tfrlem9  6580  nndi  6749  mulcanpig  7692  lediv2a  9215  seq3id3  10939  resqrexlemdecn  11756  ndvdssub  12675  bitsinv1  12707  nn0seqcvgd  12797  modprm0  13011  mplbasss  15010  fiinopn  15028  xmetunirn  15382  mopnval  15466  plyssc  15763  2lgsoddprm  16146  uspgrushgr  16335  uspgrupgr  16336  usgruspgr  16338  usgredg2vlem2  16378  ax1hfs  17029