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

Metamath Proof Explorer

Theorem imbi2d

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993)

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

Step	Hyp	Ref	Expression
1		imbid.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2	1	a1d	$⊢ φ \to (θ \to (ψ \leftrightarrow χ))$
3	2	pm5.74d	$⊢ φ \to ((θ \to ψ) \leftrightarrow (θ \to χ))$