syl333anc

Description: A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012)

	Ref	Expression
Hypotheses	syl3anc.1	$⊢ φ \to ψ$
	syl3anc.2	$⊢ φ \to χ$
	syl3anc.3	$⊢ φ \to θ$
	syl3Xanc.4	$⊢ φ \to τ$
	syl23anc.5	$⊢ φ \to η$
	syl33anc.6	$⊢ φ \to ζ$
	syl133anc.7	$⊢ φ \to σ$
	syl233anc.8	$⊢ φ \to ρ$
	syl333anc.9	$⊢ φ \to μ$
	syl333anc.10	$⊢ ((ψ \land χ \land θ) \land (τ \land η \land ζ) \land (σ \land ρ \land μ)) \to λ$
Assertion	syl333anc	$⊢ φ \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		syl133anc.7	$⊢ φ \to σ$
8		syl233anc.8	$⊢ φ \to ρ$
9		syl333anc.9	$⊢ φ \to μ$
10		syl333anc.10	$⊢ ((ψ \land χ \land θ) \land (τ \land η \land ζ) \land (σ \land ρ \land μ)) \to λ$
11	7 8 9	3jca	$⊢ φ \to (σ \land ρ \land μ)$
12	1 2 3 4 5 6 11 10	syl331anc	$⊢ φ \to λ$

Metamath Proof Explorer