pm5.53

Description: Theorem *5.53 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005)

		Ref	Expression
	Assertion	pm5.53	$⊢ (((φ \lor ψ) \lor χ) \to θ) \leftrightarrow (((φ \to θ) \land (ψ \to θ)) \land (χ \to θ))$

Step	Hyp	Ref	Expression
1		jaob	$⊢ (((φ \lor ψ) \lor χ) \to θ) \leftrightarrow (((φ \lor ψ) \to θ) \land (χ \to θ))$
2		jaob	$⊢ ((φ \lor ψ) \to θ) \leftrightarrow ((φ \to θ) \land (ψ \to θ))$
3	2	anbi1i	$⊢ (((φ \lor ψ) \to θ) \land (χ \to θ)) \leftrightarrow (((φ \to θ) \land (ψ \to θ)) \land (χ \to θ))$
4	1 3	bitri	$⊢ (((φ \lor ψ) \lor χ) \to θ) \leftrightarrow (((φ \to θ) \land (ψ \to θ)) \land (χ \to θ))$

Metamath Proof Explorer