This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem syl231anc

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012)

	Ref	Expression
Hypotheses	syl3anc.1	$⊢ φ \to ψ$
	syl3anc.2	$⊢ φ \to χ$
	syl3anc.3	$⊢ φ \to θ$
	syl3Xanc.4	$⊢ φ \to τ$
	syl23anc.5	$⊢ φ \to η$
	syl33anc.6	$⊢ φ \to ζ$
	syl231anc.7	$⊢ ((ψ \land χ) \land (θ \land τ \land η) \land ζ) \to σ$
Assertion	syl231anc	$⊢ φ \to σ$

Step	Hyp	Ref	Expression
1		syl3anc.1	$⊢ φ \to ψ$
2		syl3anc.2	$⊢ φ \to χ$
3		syl3anc.3	$⊢ φ \to θ$
4		syl3Xanc.4	$⊢ φ \to τ$
5		syl23anc.5	$⊢ φ \to η$
6		syl33anc.6	$⊢ φ \to ζ$
7		syl231anc.7	$⊢ ((ψ \land χ) \land (θ \land τ \land η) \land ζ) \to σ$
8	1 2	jca	$⊢ φ \to (ψ \land χ)$
9	8 3 4 5 6 7	syl131anc	$⊢ φ \to σ$