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  2817  vtocl2gaf  2819  vtocl3gaf  2821  ifmdc  3589  elinti  3868  copsexg  4259  nlimsucg  4580  tfisi  4601  vtoclr  4689  issref  5026  relresfld  5173  f1o2ndf1  6247  tfrlem9  6338  nndi  6505  mulcanpig  7352  lediv2a  8870  seq3id3  10525  resqrexlemdecn  11039  ndvdssub  11953  nn0seqcvgd  12059  modprm0  12272  fiinopn  13901  xmetunirn  14255  mopnval  14339  ax1hfs  15220