pm4.79

Description: Theorem *4.79 of WhiteheadRussell p. 121. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 27-Jun-2013)

		Ref	Expression
	Assertion	pm4.79	$⊢ ((ψ \to φ) \lor (χ \to φ)) \leftrightarrow ((ψ \land χ) \to φ)$

Step	Hyp	Ref	Expression
1		id	$⊢ (ψ \to φ) \to (ψ \to φ)$
2		id	$⊢ (χ \to φ) \to (χ \to φ)$
3	1 2	jaoa	$⊢ ((ψ \to φ) \lor (χ \to φ)) \to ((ψ \land χ) \to φ)$
4		simplim	$⊢ \neg (ψ \to φ) \to ψ$
5		pm3.3	$⊢ ((ψ \land χ) \to φ) \to (ψ \to (χ \to φ))$
6	4 5	syl5	$⊢ ((ψ \land χ) \to φ) \to (\neg (ψ \to φ) \to (χ \to φ))$
7	6	orrd	$⊢ ((ψ \land χ) \to φ) \to ((ψ \to φ) \lor (χ \to φ))$
8	3 7	impbii	$⊢ ((ψ \to φ) \lor (χ \to φ)) \leftrightarrow ((ψ \land χ) \to φ)$

Metamath Proof Explorer