Theorem anc2l

Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.)

Conclusion

\( \vdash (\varphi \rightarrow \psi \rightarrow \chi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \wedge \chi \)

Proof

pm5.42

biimpi _