Theorem syl221anc
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 \)
syl3Xanc.4
\( \vdash \varphi \rightarrow \tau \)
syl23anc.5
\( \vdash \varphi \rightarrow \eta \)
syl221anc.6
\( \vdash \psi \wedge \chi \wedge \theta \wedge \tau \wedge \eta \rightarrow \zeta \)
Conclusion
\( \vdash \varphi \rightarrow \zeta \)
Proof
l0
syl3anc.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl3anc.2
\( \vdash \varphi \rightarrow \chi \)
l2
syl3anc.3
syl3Xanc.4
l4
jca l2 _
\( \vdash \varphi \rightarrow \theta \wedge \tau \)
l5
syl23anc.5
\( \vdash \varphi \rightarrow \eta \)
syl221anc.6
\( \vdash \psi \wedge \chi \wedge \theta \wedge \tau \wedge \eta \rightarrow \zeta \)
syl211anc l0 l1 l4 l5 _