Metamath Proof Explorer

Theorem sylanl2

Description: A syllogism inference. (Contributed by NM, 1-Jan-2005)

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

Proof

Step	Hyp	Ref	Expression
1		sylanl2.1	$⊢ φ \to χ$
2		sylanl2.2	$⊢ ((ψ \land χ) \land θ) \to τ$
3	1	adantl	$⊢ (ψ \land φ) \to χ$
4	3 2	syldanl	$⊢ ((ψ \land φ) \land θ) \to τ$