Metamath Proof Explorer

Theorem syl2and

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		syl2and.1	$⊢ φ \to (ψ \to χ)$
2		syl2and.2	$⊢ φ \to (θ \to τ)$
3		syl2and.3	$⊢ φ \to ((χ \land τ) \to η)$
4	2 3	sylan2d	$⊢ φ \to ((χ \land θ) \to η)$
5	1 4	syland	$⊢ φ \to ((ψ \land θ) \to η)$