Metamath Proof Explorer

Theorem bibi2d

Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993) (Proof shortened by Wolf Lammen, 19-May-2013)

		Ref	Expression
	Hypothesis	imbid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	bibi2d	$⊢ φ \to ((θ \leftrightarrow ψ) \leftrightarrow (θ \leftrightarrow χ))$

Proof

Step	Hyp	Ref	Expression
1		imbid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2	1	pm5.74i	$⊢ (φ \to ψ) \leftrightarrow (φ \to χ)$
3	2	bibi2i	$⊢ ((φ \to θ) \leftrightarrow (φ \to ψ)) \leftrightarrow ((φ \to θ) \leftrightarrow (φ \to χ))$
4		pm5.74	$⊢ (φ \to (θ \leftrightarrow ψ)) \leftrightarrow ((φ \to θ) \leftrightarrow (φ \to ψ))$
5		pm5.74	$⊢ (φ \to (θ \leftrightarrow χ)) \leftrightarrow ((φ \to θ) \leftrightarrow (φ \to χ))$
6	3 4 5	3bitr4i	$⊢ (φ \to (θ \leftrightarrow ψ)) \leftrightarrow (φ \to (θ \leftrightarrow χ))$
7	6	pm5.74ri	$⊢ φ \to ((θ \leftrightarrow ψ) \leftrightarrow (θ \leftrightarrow χ))$