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  886  hbequid  1524  equidqe  1543  equid  1712  ax10  1728  hbae  1729  vtoclgaf  2826  vtocl2gaf  2828  vtocl3gaf  2830  ifmdc  3598  elinti  3880  copsexg  4274  nlimsucg  4599  tfisi  4620  vtoclr  4708  issref  5049  relresfld  5196  f1o2ndf1  6283  tfrlem9  6374  nndi  6541  mulcanpig  7397  lediv2a  8916  seq3id3  10598  resqrexlemdecn  11159  ndvdssub  12074  nn0seqcvgd  12182  modprm0  12395  fiinopn  14183  xmetunirn  14537  mopnval  14621  plyssc  14918  2lgsoddprm  15270  ax1hfs  15634