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  890  hbequid  1559  equidqe  1578  equid  1747  ax10  1763  hbae  1764  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  ifmdc  3645  elinti  3932  copsexg  4331  nlimsucg  4659  tfisi  4680  vtoclr  4769  ssrelrn  4917  issref  5114  relresfld  5261  f1o2ndf1  6385  tfrlem9  6476  nndi  6645  mulcanpig  7538  lediv2a  9058  seq3id3  10763  resqrexlemdecn  11544  ndvdssub  12462  bitsinv1  12494  nn0seqcvgd  12584  modprm0  12798  mplbasss  14681  fiinopn  14699  xmetunirn  15053  mopnval  15137  plyssc  15434  2lgsoddprm  15813  uspgrushgr  15999  uspgrupgr  16000  usgruspgr  16002  usgredg2vlem2  16042  ax1hfs  16556