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  129  ibi  176  anidms  397  pm2.13dc  890  hbequid  1559  equidqe  1578  equid  1747  ax10  1763  hbae  1764  vtoclgaf  2867  vtocl2gaf  2869  vtocl3gaf  2871  ifmdc  3646  elinti  3935  copsexg  4334  nlimsucg  4662  tfisi  4683  vtoclr  4772  ssrelrn  4920  issref  5117  relresfld  5264  f1o2ndf1  6388  tfrlem9  6480  nndi  6649  mulcanpig  7548  lediv2a  9068  seq3id3  10779  resqrexlemdecn  11566  ndvdssub  12484  bitsinv1  12516  nn0seqcvgd  12606  modprm0  12820  mplbasss  14703  fiinopn  14721  xmetunirn  15075  mopnval  15159  plyssc  15456  2lgsoddprm  15835  uspgrushgr  16024  uspgrupgr  16025  usgruspgr  16027  usgredg2vlem2  16067  ax1hfs  16635