Metamath Proof Explorer


Theorem eqeq12

Description: Equality relationship among four classes. (Contributed by NM, 3-Aug-1994)

Ref Expression
Assertion eqeq12 A = B C = D A = C B = D

Proof

Step Hyp Ref Expression
1 eqeq1 A = B A = C B = C
2 eqeq2 C = D B = C B = D
3 1 2 sylan9bb A = B C = D A = C B = D