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  2839  vtocl2gaf  2841  vtocl3gaf  2843  ifmdc  3613  elinti  3896  copsexg  4292  nlimsucg  4618  tfisi  4639  vtoclr  4727  ssrelrn  4874  issref  5070  relresfld  5217  f1o2ndf1  6321  tfrlem9  6412  nndi  6579  mulcanpig  7455  lediv2a  8975  seq3id3  10676  resqrexlemdecn  11367  ndvdssub  12285  bitsinv1  12317  nn0seqcvgd  12407  modprm0  12621  mplbasss  14502  fiinopn  14520  xmetunirn  14874  mopnval  14958  plyssc  15255  2lgsoddprm  15634  ax1hfs  16087