Metamath Proof Explorer

Theorem equequ1

Description: An equivalence law for equality. (Contributed by NM, 1-Aug-1993) (Proof shortened by Wolf Lammen, 10-Dec-2017)

Ref Expression
Assertion equequ1 
|- ( x = y -> ( x = z <-> y = z ) )

Proof

Step Hyp Ref Expression
1 ax7 
 |-  ( x = y -> ( x = z -> y = z ) )
2 equtr 
 |-  ( x = y -> ( y = z -> x = z ) )
3 1 2 impbid 
 |-  ( x = y -> ( x = z <-> y = z ) )