Theorem
anc2r
Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
Conclusion
\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \chi \wedge \varphi \)
Proof
pm3.21
imim2d
_
a2i
_
This is the content in the right pane.