Theorem imbi12i

Description: Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993)

	Ref	Expression
Hypotheses	imbi12i.1	$$⊢\phi \leftrightarrow \psi$$
	imbi12i.2	$$⊢\chi \leftrightarrow \theta$$
Assertion	imbi12i	$$⊢\left(\phi \to \chi \right)\leftrightarrow \left(\psi \to \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		imbi12i.1	$$⊢\phi \leftrightarrow \psi$$
2		imbi12i.2	$$⊢\chi \leftrightarrow \theta$$
3		imbi12	$$⊢\left(\phi \leftrightarrow \psi \right)\to \left(\left(\chi \leftrightarrow \theta \right)\to \left(\left(\phi \to \chi \right)\leftrightarrow \left(\psi \to \theta \right)\right)\right)$$
4	1 2 3	mp2	$$⊢\left(\phi \to \chi \right)\leftrightarrow \left(\psi \to \theta \right)$$