3jaob

Description: Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011) (Proof shortened by Hongxiu Chen, 29-Jun-2025)

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

Step	Hyp	Ref	Expression
1		pm5.53	$⊢ (((φ \lor χ) \lor θ) \to ψ) \leftrightarrow (((φ \to ψ) \land (χ \to ψ)) \land (θ \to ψ))$
2		df-3or	$⊢ (φ \lor χ \lor θ) \leftrightarrow ((φ \lor χ) \lor θ)$
3	2	imbi1i	$⊢ ((φ \lor χ \lor θ) \to ψ) \leftrightarrow (((φ \lor χ) \lor θ) \to ψ)$
4		df-3an	$⊢ ((φ \to ψ) \land (χ \to ψ) \land (θ \to ψ)) \leftrightarrow (((φ \to ψ) \land (χ \to ψ)) \land (θ \to ψ))$
5	1 3 4	3bitr4i	$⊢ ((φ \lor χ \lor θ) \to ψ) \leftrightarrow ((φ \to ψ) \land (χ \to ψ) \land (θ \to ψ))$

Metamath Proof Explorer