Description: Alternative proof that equality is left-Euclidean, using ax7 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | et-equeucl | ⊢ ( 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → 𝑥 = 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equid | ⊢ 𝑥 = 𝑥 | |
| 2 | ax7 | ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑥 → 𝑧 = 𝑥 ) ) | |
| 3 | 2 | com12 | ⊢ ( 𝑥 = 𝑥 → ( 𝑥 = 𝑧 → 𝑧 = 𝑥 ) ) |
| 4 | 1 3 | ax-mp | ⊢ ( 𝑥 = 𝑧 → 𝑧 = 𝑥 ) |
| 5 | equid | ⊢ 𝑦 = 𝑦 | |
| 6 | ax7 | ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝑦 → 𝑧 = 𝑦 ) ) | |
| 7 | 6 | com12 | ⊢ ( 𝑦 = 𝑦 → ( 𝑦 = 𝑧 → 𝑧 = 𝑦 ) ) |
| 8 | 5 7 | ax-mp | ⊢ ( 𝑦 = 𝑧 → 𝑧 = 𝑦 ) |
| 9 | ax7 | ⊢ ( 𝑧 = 𝑥 → ( 𝑧 = 𝑦 → 𝑥 = 𝑦 ) ) | |
| 10 | 9 | com12 | ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝑥 → 𝑥 = 𝑦 ) ) |
| 11 | 8 10 | syl | ⊢ ( 𝑦 = 𝑧 → ( 𝑧 = 𝑥 → 𝑥 = 𝑦 ) ) |
| 12 | 11 | com12 | ⊢ ( 𝑧 = 𝑥 → ( 𝑦 = 𝑧 → 𝑥 = 𝑦 ) ) |
| 13 | 4 12 | syl | ⊢ ( 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → 𝑥 = 𝑦 ) ) |