Theorem pm2.43d 50

Description: Deduction absorbing redundant antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by 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 19	. 2 ⊢ (𝜓 → 𝜓)
2		pm2.43d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒)))
3	1, 2	mpdi 43	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  loolin  101  pm2.18dc  791  sbcof2  1745  rgen2a  2440  rspct  2729  po2nr  4160  ordsuc  4407  funssres  5090  2elresin  5159  f1imass  5591  smoel  6103  tfri3  6170  nnmass  6288  sbthlem1  6746  genpcdl  7175  genpcuu  7176  recexprlemss1l  7291  recexprlemss1u  7292  uniopn  11867  elabgft1  12390  bj-rspgt  12398