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  1749  ax10  1765  hbae  1766  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  ifmdc  3648  elinti  3937  copsexg  4336  nlimsucg  4664  tfisi  4685  vtoclr  4774  ssrelrn  4922  issref  5119  relresfld  5266  f1o2ndf1  6393  tfrlem9  6485  nndi  6654  mulcanpig  7555  lediv2a  9075  seq3id3  10787  resqrexlemdecn  11574  ndvdssub  12493  bitsinv1  12525  nn0seqcvgd  12615  modprm0  12829  mplbasss  14713  fiinopn  14731  xmetunirn  15085  mopnval  15169  plyssc  15466  2lgsoddprm  15845  uspgrushgr  16034  uspgrupgr  16035  usgruspgr  16037  usgredg2vlem2  16077  ax1hfs  16709