Metamath Proof Explorer

Theorem pm2.74

Description: Theorem *2.74 of WhiteheadRussell p. 108. (Contributed by NM, 3-Jan-2005) (Proof shortened by Andrew Salmon, 7-May-2011)

		Ref	Expression
	Assertion	pm2.74	$⊢ (ψ \to φ) \to (((φ \lor ψ) \lor χ) \to (φ \lor χ))$

Step	Hyp	Ref	Expression
1		orel2	$⊢ \neg ψ \to ((φ \lor ψ) \to φ)$
2		ax-1	$⊢ φ \to ((φ \lor ψ) \to φ)$
3	1 2	ja	$⊢ (ψ \to φ) \to ((φ \lor ψ) \to φ)$
4	3	orim1d	$⊢ (ψ \to φ) \to (((φ \lor ψ) \lor χ) \to (φ \lor χ))$