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  880  hbequid  1506  equidqe  1525  equid  1694  ax10  1710  hbae  1711  vtoclgaf  2795  vtocl2gaf  2797  vtocl3gaf  2799  ifmdc  3565  elinti  3840  copsexg  4229  nlimsucg  4550  tfisi  4571  vtoclr  4659  issref  4993  relresfld  5140  f1o2ndf1  6207  tfrlem9  6298  nndi  6465  mulcanpig  7297  lediv2a  8811  seq3id3  10463  resqrexlemdecn  10976  ndvdssub  11889  nn0seqcvgd  11995  modprm0  12208  fiinopn  12796  xmetunirn  13152  mopnval  13236  ax1hfs  14103