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  890  hbequid  1559  equidqe  1578  equid  1747  ax10  1763  hbae  1764  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  ifmdc  3645  elinti  3931  copsexg  4329  nlimsucg  4657  tfisi  4678  vtoclr  4766  ssrelrn  4913  issref  5110  relresfld  5257  f1o2ndf1  6372  tfrlem9  6463  nndi  6630  mulcanpig  7518  lediv2a  9038  seq3id3  10741  resqrexlemdecn  11518  ndvdssub  12436  bitsinv1  12468  nn0seqcvgd  12558  modprm0  12772  mplbasss  14654  fiinopn  14672  xmetunirn  15026  mopnval  15110  plyssc  15407  2lgsoddprm  15786  uspgrushgr  15972  uspgrupgr  15973  usgruspgr  15975  usgredg2vlem2  16015  ax1hfs  16401