3jao

Description: Disjunction of three antecedents. (Contributed by NM, 8-Apr-1994)

		Ref	Expression
	Assertion	3jao	$⊢ ((φ \to ψ) \land (χ \to ψ) \land (θ \to ψ)) \to ((φ \lor χ \lor θ) \to ψ)$

Step	Hyp	Ref	Expression
1		jao	$⊢ (φ \to ψ) \to ((χ \to ψ) \to ((φ \lor χ) \to ψ))$
2		df-3or	$⊢ (φ \lor χ \lor θ) \leftrightarrow ((φ \lor χ) \lor θ)$
3		jao	$⊢ ((φ \lor χ) \to ψ) \to ((θ \to ψ) \to (((φ \lor χ) \lor θ) \to ψ))$
4	2 3	syl7bi	$⊢ ((φ \lor χ) \to ψ) \to ((θ \to ψ) \to ((φ \lor χ \lor θ) \to ψ))$
5	1 4	syl6	$⊢ (φ \to ψ) \to ((χ \to ψ) \to ((θ \to ψ) \to ((φ \lor χ \lor θ) \to ψ)))$
6	5	3imp	$⊢ ((φ \to ψ) \land (χ \to ψ) \land (θ \to ψ)) \to ((φ \lor χ \lor θ) \to ψ)$

Metamath Proof Explorer