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  893  hbequid  1562  equidqe  1581  equid  1749  ax10  1765  hbae  1766  vtoclgaf  2882  vtocl2gaf  2884  vtocl3gaf  2886  ifmdc  3669  elinti  3963  copsexg  4365  nlimsucg  4693  tfisi  4714  vtoclr  4803  ssrelrn  4952  issref  5150  relresfld  5297  f1o2ndf1  6437  tfrlem9  6563  nndi  6732  mulcanpig  7666  lediv2a  9189  seq3id3  10913  resqrexlemdecn  11725  ndvdssub  12644  bitsinv1  12676  nn0seqcvgd  12766  modprm0  12980  mplbasss  14980  fiinopn  14998  xmetunirn  15352  mopnval  15436  plyssc  15733  2lgsoddprm  16115  uspgrushgr  16304  uspgrupgr  16305  usgruspgr  16307  usgredg2vlem2  16347  ax1hfs  16999