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  4384  nlimsucg  4713  tfisi  4734  vtoclr  4823  ssrelrn  4972  issref  5170  relresfld  5317  f1o2ndf1  6464  tfrlem9  6590  nndi  6759  mulcanpig  7702  lediv2a  9226  seq3id3  10963  resqrexlemdecn  11780  ndvdssub  12699  bitsinv1  12731  nn0seqcvgd  12821  modprm0  13035  mplbasss  15089  fiinopn  15107  xmetunirn  15461  mopnval  15545  plyssc  15842  2lgsoddprm  16244  uspgrushgr  16433  uspgrupgr  16434  usgruspgr  16436  usgredg2vlem2  16476  ax1hfs  17136