Theorem opeq12

Description: Equality theorem for ordered pairs. (Contributed by NM, 28-May-1995)

	Ref	Expression
Assertion	opeq12	$$⊢\left(A=C\wedge B=D\right)\to ⟨A,B⟩=⟨C,D⟩$$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$$⊢A=C\to ⟨A,B⟩=⟨C,B⟩$$
2		opeq2	$$⊢B=D\to ⟨C,B⟩=⟨C,D⟩$$
3	1 2	sylan9eq	$$⊢\left(A=C\wedge B=D\right)\to ⟨A,B⟩=⟨C,D⟩$$