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  889  hbequid  1539  equidqe  1558  equid  1727  ax10  1743  hbae  1744  vtoclgaf  2846  vtocl2gaf  2848  vtocl3gaf  2850  ifmdc  3625  elinti  3911  copsexg  4309  nlimsucg  4635  tfisi  4656  vtoclr  4744  ssrelrn  4891  issref  5087  relresfld  5234  f1o2ndf1  6344  tfrlem9  6435  nndi  6602  mulcanpig  7490  lediv2a  9010  seq3id3  10713  resqrexlemdecn  11489  ndvdssub  12407  bitsinv1  12439  nn0seqcvgd  12529  modprm0  12743  mplbasss  14625  fiinopn  14643  xmetunirn  14997  mopnval  15081  plyssc  15378  2lgsoddprm  15757  uspgrushgr  15943  uspgrupgr  15944  usgruspgr  15946  usgredg2vlem2  15986  ax1hfs  16353