Description: Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl . (Contributed by NM, 12-Aug-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by BJ, 11-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | equtr2 | |- ( ( x = z /\ y = z ) -> x = y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equeucl | |- ( x = z -> ( y = z -> x = y ) ) |
|
| 2 | 1 | imp | |- ( ( x = z /\ y = z ) -> x = y ) |