Theorem pm2.43a

Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.)

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