Metamath Proof Explorer

Theorem sylanl1

Description: A syllogism inference. (Contributed by NM, 10-Mar-2005)

		Ref	Expression
	Hypotheses	sylanl1.1	$⊢ φ \to ψ$
		sylanl1.2	$⊢ ((ψ \land χ) \land θ) \to τ$
	Assertion	sylanl1	$⊢ ((φ \land χ) \land θ) \to τ$

Proof

Step	Hyp	Ref	Expression
1		sylanl1.1	$⊢ φ \to ψ$
2		sylanl1.2	$⊢ ((ψ \land χ) \land θ) \to τ$
3	1	anim1i	$⊢ (φ \land χ) \to (ψ \land χ)$
4	3 2	sylan	$⊢ ((φ \land χ) \land θ) \to τ$