Metamath Proof Explorer

Theorem wl-aetr

Description: A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019)

Ref Expression
Assertion wl-aetr ⊢ ∀ x x = y → ∀ x x = z → ∀ y y = z

Proof

Step Hyp Ref Expression
1 ax7 ⊢ x = y → x = z → y = z
2 1 al2imi ⊢ ∀ x x = y → ∀ x x = z → ∀ x y = z
3 axc11 ⊢ ∀ x x = y → ∀ x y = z → ∀ y y = z
4 2 3 syld ⊢ ∀ x x = y → ∀ x x = z → ∀ y y = z