Description: Equality relationship among four classes. (Contributed by NM, 3-Aug-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | eqeq12 | |- ( ( A = B /\ C = D ) -> ( A = C <-> B = D ) ) |
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 ) ) |