Metamath Proof Explorer

Theorem pm5.33

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

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

Step	Hyp	Ref	Expression
1		ibar	$⊢ φ \to (ψ \leftrightarrow (φ \land ψ))$
2	1	imbi1d	$⊢ φ \to ((ψ \to χ) \leftrightarrow ((φ \land ψ) \to χ))$
3	2	pm5.32i	$⊢ (φ \land (ψ \to χ)) \leftrightarrow (φ \land ((φ \land ψ) \to χ))$