Theorem anim12d1

Variant of anim12d where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010.)

Hypotheses
anim12d1.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
anim12d1.2
\( \vdash \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \theta \rightarrow \chi \wedge \tau \)
Proof
l0
anim12d1.1
anim12d1.2
a1i _
anim12d l0 _