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 
|- ( A. x x = y -> ( A. x x = z -> A. y y = z ) )

Proof

Step Hyp Ref Expression
1 ax7 
 |-  ( x = y -> ( x = z -> y = z ) )
2 1 al2imi 
 |-  ( A. x x = y -> ( A. x x = z -> A. x y = z ) )
3 axc11 
 |-  ( A. x x = y -> ( A. x y = z -> A. y y = z ) )
4 2 3 syld 
 |-  ( A. x x = y -> ( A. x x = z -> A. y y = z ) )