Theorem equequ1 1595

Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem equequ1

Step	Hyp	Ref	Expression
1		ax-8 1392	. 2 |- (x = y -> (x = z -> y = z))
2		equtr 1592	. 2 |- (x = y -> (y = z -> x = z))
3	1, 2	impbid 120	1 |- (x = y -> (x = z <-> y = z))

Syntax hints:   -> wi 4   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1335  ax-ie2 1380  ax-8 1392  ax-17 1416  ax-i9 1420

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  equveli  1639  drsb1  1677  equsb3lem  1821  euequ1  1992  axext3  2020  reu6  2724  reu7  2730  cbviota  4815  dff13f  5352  poxp  5794