Metamath Proof Explorer

Theorem syl2ani

Description: A syllogism inference. (Contributed by NM, 3-Aug-1999)

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

Proof

Step	Hyp	Ref	Expression
1		syl2ani.1	$⊢ φ \to χ$
2		syl2ani.2	$⊢ η \to θ$
3		syl2ani.3	$⊢ ψ \to ((χ \land θ) \to τ)$
4	2 3	sylan2i	$⊢ ψ \to ((χ \land η) \to τ)$
5	1 4	sylani	$⊢ ψ \to ((φ \land η) \to τ)$