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  128  ibi  175  anidms  395  pm2.13dc  875  hbequid  1501  equidqe  1520  equid  1689  ax10  1705  hbae  1706  vtoclgaf  2790  vtocl2gaf  2792  vtocl3gaf  2794  ifmdc  3557  elinti  3832  copsexg  4221  nlimsucg  4542  tfisi  4563  vtoclr  4651  issref  4985  relresfld  5132  f1o2ndf1  6192  tfrlem9  6283  nndi  6450  mulcanpig  7272  lediv2a  8786  seq3id3  10438  resqrexlemdecn  10950  ndvdssub  11863  nn0seqcvgd  11969  modprm0  12182  fiinopn  12602  xmetunirn  12958  mopnval  13042  ax1hfs  13910