Theorem cdeqim

Description: Distribute conditional equality over implication. (Contributed by Mario Carneiro, 11-Aug-2016)

	Ref	Expression
Hypotheses	cdeqnot.1	|- CondEq ( x = y -> ( ph <-> ps ) )
	cdeqim.1	|- CondEq ( x = y -> ( ch <-> th ) )
Assertion	cdeqim	|- CondEq ( x = y -> ( ( ph -> ch ) <-> ( ps -> th ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdeqnot.1	|- CondEq ( x = y -> ( ph <-> ps ) )
2		cdeqim.1	|- CondEq ( x = y -> ( ch <-> th ) )
3	1	cdeqri	|- ( x = y -> ( ph <-> ps ) )
4	2	cdeqri	|- ( x = y -> ( ch <-> th ) )
5	3 4	imbi12d	|- ( x = y -> ( ( ph -> ch ) <-> ( ps -> th ) ) )
6	5	cdeqi	|- CondEq ( x = y -> ( ( ph -> ch ) <-> ( ps -> th ) ) )