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  887  hbequid  1537  equidqe  1556  equid  1725  ax10  1741  hbae  1742  vtoclgaf  2843  vtocl2gaf  2845  vtocl3gaf  2847  ifmdc  3622  elinti  3908  copsexg  4306  nlimsucg  4632  tfisi  4653  vtoclr  4741  ssrelrn  4888  issref  5084  relresfld  5231  f1o2ndf1  6337  tfrlem9  6428  nndi  6595  mulcanpig  7483  lediv2a  9003  seq3id3  10706  resqrexlemdecn  11438  ndvdssub  12356  bitsinv1  12388  nn0seqcvgd  12478  modprm0  12692  mplbasss  14573  fiinopn  14591  xmetunirn  14945  mopnval  15029  plyssc  15326  2lgsoddprm  15705  ax1hfs  16215