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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  sylc  62  impbid  128  ibi  175  anidms  392  pm2.13dc  853  hbequid  1476  equidqe  1495  equid  1660  ax10  1678  hbae  1679  vtoclgaf  2722  vtocl2gaf  2724  vtocl3gaf  2726  ifmdc  3475  elinti  3746  copsexg  4126  nlimsucg  4441  tfisi  4461  vtoclr  4547  issref  4879  relresfld  5026  f1o2ndf1  6079  tfrlem9  6170  nndi  6336  mulcanpig  7091  lediv2a  8563  seq3id3  10173  resqrexlemdecn  10676  ndvdssub  11475  nn0seqcvgd  11568  fiinopn  12014  xmetunirn  12347  mopnval  12431  ax1hfs  12931