3jaob

Description: Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011)

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

Step	Hyp	Ref	Expression
1		3mix1	$⊢ φ \to (φ \lor χ \lor θ)$
2	1	imim1i	$⊢ ((φ \lor χ \lor θ) \to ψ) \to (φ \to ψ)$
3		3mix2	$⊢ χ \to (φ \lor χ \lor θ)$
4	3	imim1i	$⊢ ((φ \lor χ \lor θ) \to ψ) \to (χ \to ψ)$
5		3mix3	$⊢ θ \to (φ \lor χ \lor θ)$
6	5	imim1i	$⊢ ((φ \lor χ \lor θ) \to ψ) \to (θ \to ψ)$
7	2 4 6	3jca	$⊢ ((φ \lor χ \lor θ) \to ψ) \to ((φ \to ψ) \land (χ \to ψ) \land (θ \to ψ))$
8		3jao	$⊢ ((φ \to ψ) \land (χ \to ψ) \land (θ \to ψ)) \to ((φ \lor χ \lor θ) \to ψ)$
9	7 8	impbii	$⊢ ((φ \lor χ \lor θ) \to ψ) \leftrightarrow ((φ \to ψ) \land (χ \to ψ) \land (θ \to ψ))$

Metamath Proof Explorer