This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imbi12d

Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 16-May-1993)

	Ref	Expression
Hypotheses	imbi12d.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	imbi12d.2	$⊢ φ \to (θ \leftrightarrow τ)$
Assertion	imbi12d	$⊢ φ \to ((ψ \to θ) \leftrightarrow (χ \to τ))$

Step	Hyp	Ref	Expression
1		imbi12d.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		imbi12d.2	$⊢ φ \to (θ \leftrightarrow τ)$
3	1	imbi1d	$⊢ φ \to ((ψ \to θ) \leftrightarrow (χ \to θ))$
4	2	imbi2d	$⊢ φ \to ((χ \to θ) \leftrightarrow (χ \to τ))$
5	3 4	bitrd	$⊢ φ \to ((ψ \to θ) \leftrightarrow (χ \to τ))$