Theorem imbi12i

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

	Ref	Expression
Hypotheses	imbi12i.1	⊢ ( 𝜑 ↔ 𝜓 )
	imbi12i.2	⊢ ( 𝜒 ↔ 𝜃 )
Assertion	imbi12i	⊢ ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		imbi12i.1	⊢ ( 𝜑 ↔ 𝜓 )
2		imbi12i.2	⊢ ( 𝜒 ↔ 𝜃 )
3		imbi12	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜒 ↔ 𝜃 ) → ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) ) ) )
4	1 2 3	mp2	⊢ ( ( 𝜑 → 𝜒 ) ↔ ( 𝜓 → 𝜃 ) )