Theorem imbi12i

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

	Ref	Expression
Hypotheses	imbi12i.1	|- ( ph <-> ps )
	imbi12i.2	|- ( ch <-> th )
Assertion	imbi12i	|- ( ( ph -> ch ) <-> ( ps -> th ) )

Proof

Step	Hyp	Ref	Expression
1		imbi12i.1	|- ( ph <-> ps )
2		imbi12i.2	|- ( ch <-> th )
3		imbi12	|- ( ( ph <-> ps ) -> ( ( ch <-> th ) -> ( ( ph -> ch ) <-> ( ps -> th ) ) ) )
4	1 2 3	mp2	|- ( ( ph -> ch ) <-> ( ps -> th ) )