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  2879  vtocl2gaf  2881  vtocl3gaf  2883  ifmdc  3664  elinti  3957  copsexg  4359  nlimsucg  4687  tfisi  4708  vtoclr  4797  ssrelrn  4946  issref  5144  relresfld  5291  f1o2ndf1  6423  tfrlem9  6549  nndi  6718  mulcanpig  7646  lediv2a  9165  seq3id3  10882  resqrexlemdecn  11690  ndvdssub  12609  bitsinv1  12641  nn0seqcvgd  12731  modprm0  12945  mplbasss  14838  fiinopn  14856  xmetunirn  15210  mopnval  15294  plyssc  15591  2lgsoddprm  15973  uspgrushgr  16162  uspgrupgr  16163  usgruspgr  16165  usgredg2vlem2  16205  ax1hfs  16857