Metamath Proof Explorer

Theorem pm5.74

Description: Distribution of implication over biconditional. Theorem *5.74 of WhiteheadRussell p. 126. (Contributed by NM, 1-Aug-1994) (Proof shortened by Wolf Lammen, 11-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		biimp	$⊢ (ψ \leftrightarrow χ) \to (ψ \to χ)$
2	1	imim3i	$⊢ (φ \to (ψ \leftrightarrow χ)) \to ((φ \to ψ) \to (φ \to χ))$
3		biimpr	$⊢ (ψ \leftrightarrow χ) \to (χ \to ψ)$
4	3	imim3i	$⊢ (φ \to (ψ \leftrightarrow χ)) \to ((φ \to χ) \to (φ \to ψ))$
5	2 4	impbid	$⊢ (φ \to (ψ \leftrightarrow χ)) \to ((φ \to ψ) \leftrightarrow (φ \to χ))$
6		biimp	$⊢ ((φ \to ψ) \leftrightarrow (φ \to χ)) \to ((φ \to ψ) \to (φ \to χ))$
7	6	pm2.86d	$⊢ ((φ \to ψ) \leftrightarrow (φ \to χ)) \to (φ \to (ψ \to χ))$
8		biimpr	$⊢ ((φ \to ψ) \leftrightarrow (φ \to χ)) \to ((φ \to χ) \to (φ \to ψ))$
9	8	pm2.86d	$⊢ ((φ \to ψ) \leftrightarrow (φ \to χ)) \to (φ \to (χ \to ψ))$
10	7 9	impbidd	$⊢ ((φ \to ψ) \leftrightarrow (φ \to χ)) \to (φ \to (ψ \leftrightarrow χ))$
11	5 10	impbii	$⊢ (φ \to (ψ \leftrightarrow χ)) \leftrightarrow ((φ \to ψ) \leftrightarrow (φ \to χ))$