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  1527  equidqe  1546  equid  1715  ax10  1731  hbae  1732  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  ifmdc  3602  elinti  3884  copsexg  4278  nlimsucg  4603  tfisi  4624  vtoclr  4712  issref  5053  relresfld  5200  f1o2ndf1  6295  tfrlem9  6386  nndi  6553  mulcanpig  7419  lediv2a  8939  seq3id3  10633  resqrexlemdecn  11194  ndvdssub  12112  bitsinv1  12144  nn0seqcvgd  12234  modprm0  12448  fiinopn  14324  xmetunirn  14678  mopnval  14762  plyssc  15059  2lgsoddprm  15438  ax1hfs  15805