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  886  hbequid  1527  equidqe  1546  equid  1715  ax10  1731  hbae  1732  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  ifmdc  3601  elinti  3883  copsexg  4277  nlimsucg  4602  tfisi  4623  vtoclr  4711  issref  5052  relresfld  5199  f1o2ndf1  6286  tfrlem9  6377  nndi  6544  mulcanpig  7402  lediv2a  8922  seq3id3  10616  resqrexlemdecn  11177  ndvdssub  12095  nn0seqcvgd  12209  modprm0  12423  fiinopn  14240  xmetunirn  14594  mopnval  14678  plyssc  14975  2lgsoddprm  15354  ax1hfs  15718