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  892  hbequid  1561  equidqe  1580  equid  1748  ax10  1764  hbae  1765  vtoclgaf  2868  vtocl2gaf  2870  vtocl3gaf  2872  ifmdc  3649  elinti  3938  copsexg  4338  nlimsucg  4666  tfisi  4687  vtoclr  4776  ssrelrn  4924  issref  5121  relresfld  5268  f1o2ndf1  6398  tfrlem9  6490  nndi  6659  mulcanpig  7560  lediv2a  9080  seq3id3  10792  resqrexlemdecn  11595  ndvdssub  12514  bitsinv1  12546  nn0seqcvgd  12636  modprm0  12850  mplbasss  14739  fiinopn  14757  xmetunirn  15111  mopnval  15195  plyssc  15492  2lgsoddprm  15871  uspgrushgr  16060  uspgrupgr  16061  usgruspgr  16063  usgredg2vlem2  16103  ax1hfs  16756