Theorem 2a1i

Inference introducing two antecedents. Two applications of a1i. Inference associated with 2a1. (Contributed by Jeff Hankins, 4-Aug-2009.)

Hypothesis
2a1i.1
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \rightarrow \chi \rightarrow \varphi \)
Proof
2a1i.1
a1i _
a1i _