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

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

This theorem is referenced by:  sylc  61  impbid  127  ibi  174  anidms  389  pm2.13dc  812  hbequid  1446  equidqe  1465  equid  1629  ax10  1645  hbae  1646  vtoclgaf  2663  vtocl2gaf  2665  vtocl3gaf  2667  elinti  3645  copsexg  3999  nlimsucg  4309  tfisi  4328  vtoclr  4406  issref  4727  relresfld  4867  f1o2ndf1  5869  tfrlem9  5958  nndi  6088  mulcanpig  6525  lediv2a  7973  iseqid3s  9466  resqrexlemdecn  9898  ndvdssub  10330  nn0seqcvgd  10423  ax1hfs  10786