Metamath Proof Explorer

Theorem imbi1d

Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993) (Proof shortened by Wolf Lammen, 17-Sep-2013)

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

Proof

Step	Hyp	Ref	Expression
1		imbid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2	1	biimprd	$⊢ φ \to (χ \to ψ)$
3	2	imim1d	$⊢ φ \to ((ψ \to θ) \to (χ \to θ))$
4	1	biimpd	$⊢ φ \to (ψ \to χ)$
5	4	imim1d	$⊢ φ \to ((χ \to θ) \to (ψ \to θ))$
6	3 5	impbid	$⊢ φ \to ((ψ \to θ) \leftrightarrow (χ \to θ))$