Theorem
syl3anc
Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
syl3anc.1
\( \vdash \varphi \rightarrow \psi \)
syl3anc.2
\( \vdash \varphi \rightarrow \chi \)
syl3anc.3
\( \vdash \varphi \rightarrow \theta \)
syl3anc.4
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \tau \)
Proof
l0
syl3anc.1
l1
syl3anc.2
syl3anc.3
l3
3jca
l0
l1
_
\( \vdash \varphi \rightarrow \psi \wedge \chi \wedge \theta \)
syl3anc.4
\( \vdash \psi \wedge \chi \wedge \theta \rightarrow \tau \)
syl
l3
_
This is the content in the right pane.