Theorem 2a1

A double form of [ax-1]. Its associated inference is 2a1i. Its associated deduction is 2a1d. (Contributed by BJ, 10-Aug-2020.) (Proof shortened by Wolf Lammen, 1-Sep-2020.)

Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \varphi \)
Proof
id
2a1d _