Theorem pm2.43i 48

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  61  impbid  127  ibi  174  anidms  389  pm2.13dc  813  hbequid  1447  equidqe  1466  equid  1630  ax10  1646  hbae  1647  vtoclgaf  2664  vtocl2gaf  2666  vtocl3gaf  2668  elinti  3653  copsexg  4007  nlimsucg  4317  tfisi  4336  vtoclr  4414  issref  4737  relresfld  4877  f1o2ndf1  5880  tfrlem9  5968  nndi  6130  mulcanpig  6587  lediv2a  8040  iseqid3s  9562  resqrexlemdecn  10036  ndvdssub  10474  nn0seqcvgd  10567  ax1hfs  10944