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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  sylc  62  impbid  129  ibi  176  anidms  401  pm2.13dc  897  hbequid  1566  equidqe  1585  equid  1753  ax10  1769  hbae  1770  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  ifmdc  3683  elinti  3979  copsexg  4386  nlimsucg  4715  tfisi  4736  vtoclr  4825  ssrelrn  4974  issref  5173  relresfld  5320  f1o2ndf1  6468  tfrlem9  6594  nndi  6763  mulcanpig  7709  lediv2a  9234  seq3id3  10983  resqrexlemdecn  11801  ndvdssub  12723  bitsinv1  12755  nn0seqcvgd  12845  modprm0  13063  mplbasss  15224  fiinopn  15242  xmetunirn  15596  mopnval  15680  plyssc  15977  2lgsoddprm  16449  uspgrushgr  16638  uspgrupgr  16639  usgruspgr  16641  usgredg2vlem2  16681  ax1hfs  17343