Theorem sylancom

Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)

Hypotheses
sylancom.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
sylancom.2
\( \vdash \chi \wedge \psi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \theta \)
Proof
l0
sylancom.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
l1
simpr
\( \vdash \varphi \wedge \psi \rightarrow \psi \)
sylancom.2
\( \vdash \chi \wedge \psi \rightarrow \theta \)
syl2anc l0 l1 _