Theorem eqeqan2d

Description: Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019)

	Ref	Expression
Hypothesis	eqeqan2d.1	|- ( ph -> C = D )
Assertion	eqeqan2d	|- ( ( A = B /\ ph ) -> ( A = C <-> B = D ) )

Proof

Step	Hyp	Ref	Expression
1		eqeqan2d.1	|- ( ph -> C = D )
2		eqeq12	|- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) )
3	1 2	sylan2	|- ( ( A = B /\ ph ) -> ( A = C <-> B = D ) )