Metamath Proof Explorer

Theorem 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	1 2	bianbi	$⊢ (((φ \lor ψ) \lor χ) \to θ) \leftrightarrow (((φ \to θ) \land (ψ \to θ)) \land (χ \to θ))$