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  401  pm2.13dc  897  hbequid  1566  equidqe  1585  equid  1753  ax10  1769  hbae  1770  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  ifmdc  3683  elinti  3977  copsexg  4382  nlimsucg  4711  tfisi  4732  vtoclr  4821  ssrelrn  4970  issref  5168  relresfld  5315  f1o2ndf1  6458  tfrlem9  6584  nndi  6753  mulcanpig  7696  lediv2a  9219  seq3id3  10944  resqrexlemdecn  11761  ndvdssub  12680  bitsinv1  12712  nn0seqcvgd  12802  modprm0  13016  mplbasss  15070  fiinopn  15088  xmetunirn  15442  mopnval  15526  plyssc  15823  2lgsoddprm  16215  uspgrushgr  16404  uspgrupgr  16405  usgruspgr  16407  usgredg2vlem2  16447  ax1hfs  17098