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  2866  vtocl2gaf  2868  vtocl3gaf  2870  ifmdc  3645  elinti  3932  copsexg  4330  nlimsucg  4658  tfisi  4679  vtoclr  4767  ssrelrn  4914  issref  5111  relresfld  5258  f1o2ndf1  6380  tfrlem9  6471  nndi  6640  mulcanpig  7530  lediv2a  9050  seq3id3  10754  resqrexlemdecn  11531  ndvdssub  12449  bitsinv1  12481  nn0seqcvgd  12571  modprm0  12785  mplbasss  14668  fiinopn  14686  xmetunirn  15040  mopnval  15124  plyssc  15421  2lgsoddprm  15800  uspgrushgr  15986  uspgrupgr  15987  usgruspgr  15989  usgredg2vlem2  16029  ax1hfs  16472