Theorem pm2.43d 53

Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 56 and pm2.43i 52. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)

Hypothesis

Ref	Expression
pm2.43d.1	⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
pm2.43d	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem pm2.43d

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 45	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:  loolin  111  rspct  3577  po2nr  5563  somo  5588  ordelord  6357  tz7.7  6361  funssres  6563  2elresin  6642  dffv2  6959  f1imass  7242  onint  7769  onfununi  8313  smoel  8332  tfrlem11  8359  tfr3  8370  omass  8547  nnmass  8591  sbthlem1  9057  pssnn  9138  php  9177  inf3lem2  9589  cardne  9925  dfac2b  10091  indpi  10867  genpcd  10966  ltexprlem7  11002  addcanpr  11006  reclem4pr  11010  suplem2pr  11013  sup2  12146  nnunb  12445  uzwo  12877  xrub  13279  grpid  18914  lsmcss  21608  uniopn  22791  fclsss1  23916  fclsss2  23917  sltval2  27575  grpoid  30456  spansncvi  31588  pjnormssi  32104  sumdmdlem2  32355  acycgrcycl  35141  meran1  36406  bj-animbi  36554  currysetlem2  36943  bj-elsn0  37150  poimirlem31  37652  heicant  37656  hlhilhillem  41961  sn-sup2  42486  ee223  44631  eel2122old  44714  afv0nbfvbi  47156  fmtnoprmfac1lem  47569