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  3667  elinti  3960  copsexg  4362  nlimsucg  4690  tfisi  4711  vtoclr  4800  ssrelrn  4949  issref  5147  relresfld  5294  f1o2ndf1  6426  tfrlem9  6552  nndi  6721  mulcanpig  7655  lediv2a  9174  seq3id3  10893  resqrexlemdecn  11705  ndvdssub  12624  bitsinv1  12656  nn0seqcvgd  12746  modprm0  12960  mplbasss  14900  fiinopn  14918  xmetunirn  15272  mopnval  15356  plyssc  15653  2lgsoddprm  16035  uspgrushgr  16224  uspgrupgr  16225  usgruspgr  16227  usgredg2vlem2  16267  ax1hfs  16920