Metamath Proof Explorer

Theorem jaob

Description: Disjunction of antecedents. Compare Theorem *4.77 of WhiteheadRussell p. 121. (Contributed by NM, 30-May-1994) (Proof shortened by Wolf Lammen, 9-Dec-2012)

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

Proof

Step	Hyp	Ref	Expression
1		pm2.67-2	$⊢ ((φ \lor χ) \to ψ) \to (φ \to ψ)$
2		olc	$⊢ χ \to (φ \lor χ)$
3	2	imim1i	$⊢ ((φ \lor χ) \to ψ) \to (χ \to ψ)$
4	1 3	jca	$⊢ ((φ \lor χ) \to ψ) \to ((φ \to ψ) \land (χ \to ψ))$
5		pm3.44	$⊢ ((φ \to ψ) \land (χ \to ψ)) \to ((φ \lor χ) \to ψ)$
6	4 5	impbii	$⊢ ((φ \lor χ) \to ψ) \leftrightarrow ((φ \to ψ) \land (χ \to ψ))$