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  394  pm2.13dc  870  hbequid  1493  equidqe  1512  equid  1677  ax10  1695  hbae  1696  vtoclgaf  2751  vtocl2gaf  2753  vtocl3gaf  2755  ifmdc  3509  elinti  3780  copsexg  4166  nlimsucg  4481  tfisi  4501  vtoclr  4587  issref  4921  relresfld  5068  f1o2ndf1  6125  tfrlem9  6216  nndi  6382  mulcanpig  7143  lediv2a  8653  seq3id3  10280  resqrexlemdecn  10784  ndvdssub  11627  nn0seqcvgd  11722  fiinopn  12171  xmetunirn  12527  mopnval  12611  ax1hfs  13240