pm5.32

Description: Distribution of implication over biconditional. Theorem *5.32 of WhiteheadRussell p. 125. (Contributed by NM, 1-Aug-1994)

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

Step	Hyp	Ref	Expression
1		notbi	$⊢ (ψ \leftrightarrow χ) \leftrightarrow (\neg ψ \leftrightarrow \neg χ)$
2	1	imbi2i	$⊢ (φ \to (ψ \leftrightarrow χ)) \leftrightarrow (φ \to (\neg ψ \leftrightarrow \neg χ))$
3		pm5.74	$⊢ (φ \to (\neg ψ \leftrightarrow \neg χ)) \leftrightarrow ((φ \to \neg ψ) \leftrightarrow (φ \to \neg χ))$
4		notbi	$⊢ ((φ \to \neg ψ) \leftrightarrow (φ \to \neg χ)) \leftrightarrow (\neg (φ \to \neg ψ) \leftrightarrow \neg (φ \to \neg χ))$
5	2 3 4	3bitri	$⊢ (φ \to (ψ \leftrightarrow χ)) \leftrightarrow (\neg (φ \to \neg ψ) \leftrightarrow \neg (φ \to \neg χ))$
6		df-an	$⊢ (φ \land ψ) \leftrightarrow \neg (φ \to \neg ψ)$
7		df-an	$⊢ (φ \land χ) \leftrightarrow \neg (φ \to \neg χ)$
8	6 7	bibi12i	$⊢ ((φ \land ψ) \leftrightarrow (φ \land χ)) \leftrightarrow (\neg (φ \to \neg ψ) \leftrightarrow \neg (φ \to \neg χ))$
9	5 8	bitr4i	$⊢ (φ \to (ψ \leftrightarrow χ)) \leftrightarrow ((φ \land ψ) \leftrightarrow (φ \land χ))$

Metamath Proof Explorer