Theorem cdeqeq

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

	Ref	Expression
Hypotheses	cdeqeq.1	|- CondEq ( x = y -> A = B )
	cdeqeq.2	|- CondEq ( x = y -> C = D )
Assertion	cdeqeq	|- CondEq ( x = y -> ( A = C <-> B = D ) )

Proof

Step	Hyp	Ref	Expression
1		cdeqeq.1	|- CondEq ( x = y -> A = B )
2		cdeqeq.2	|- CondEq ( x = y -> C = D )
3	1	cdeqri	|- ( x = y -> A = B )
4	2	cdeqri	|- ( x = y -> C = D )
5	3 4	eqeq12d	|- ( x = y -> ( A = C <-> B = D ) )
6	5	cdeqi	|- CondEq ( x = y -> ( A = C <-> B = D ) )