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	⊢ (𝜑 → (𝜑 → 𝜓))

Assertion

Ref	Expression
pm2.43i	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.43i

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜑 → 𝜑)
2		pm2.43i.1	. 2 ⊢ (𝜑 → (𝜑 → 𝜓))
3	1, 2	mpd 13	1 ⊢ (𝜑 → 𝜓)

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  871  hbequid  1494  equidqe  1513  equid  1678  ax10  1696  hbae  1697  vtoclgaf  2754  vtocl2gaf  2756  vtocl3gaf  2758  ifmdc  3514  elinti  3788  copsexg  4174  nlimsucg  4489  tfisi  4509  vtoclr  4595  issref  4929  relresfld  5076  f1o2ndf1  6133  tfrlem9  6224  nndi  6390  mulcanpig  7167  lediv2a  8677  seq3id3  10311  resqrexlemdecn  10816  ndvdssub  11663  nn0seqcvgd  11758  fiinopn  12210  xmetunirn  12566  mopnval  12650  ax1hfs  13431