pm4.87

Description: Theorem *4.87 of WhiteheadRussell p. 122. (Contributed by NM, 3-Jan-2005) (Proof shortened by Eric Schmidt, 26-Oct-2006)

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

Step	Hyp	Ref	Expression
1		impexp	$⊢ ((φ \land ψ) \to χ) \leftrightarrow (φ \to (ψ \to χ))$
2		bi2.04	$⊢ (φ \to (ψ \to χ)) \leftrightarrow (ψ \to (φ \to χ))$
3	1 2	pm3.2i	$⊢ ((((φ \land ψ) \to χ) \leftrightarrow (φ \to (ψ \to χ))) \land ((φ \to (ψ \to χ)) \leftrightarrow (ψ \to (φ \to χ))))$
4		impexp	$⊢ ((ψ \land φ) \to χ) \leftrightarrow (ψ \to (φ \to χ))$
5	4	bicomi	$⊢ (ψ \to (φ \to χ)) \leftrightarrow ((ψ \land φ) \to χ)$
6	3 5	pm3.2i	$⊢ (((((φ \land ψ) \to χ) \leftrightarrow (φ \to (ψ \to χ))) \land ((φ \to (ψ \to χ)) \leftrightarrow (ψ \to (φ \to χ)))) \land ((ψ \to (φ \to χ)) \leftrightarrow ((ψ \land φ) \to χ)))$

Metamath Proof Explorer