Theorem pm2.43d

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

Hypothesis
pm2.43d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Proof
l0
id
\( \vdash \psi \rightarrow \psi \)
pm2.43d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \psi \rightarrow \chi \)
mpdi l0 _