Theorem equequ1 1689

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 1483	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1686	. 2 |- ( x = y -> ( y = z -> x = z ) )
3	1, 2	impbid 128	1 |- ( x = y -> ( x = z <-> y = z ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ie2 1471  ax-8 1483  ax-17 1507  ax-i9 1511

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equveli  1733  drsb1  1772  equsb3lem  1924  euequ1  2095  axext3  2123  reu6  2877  reu7  2883  disjiun  3932  cbviota  5101  dff13f  5679  poxp  6137  dcdifsnid  6408  supmoti  6888  isoti  6902  fsum2dlemstep  11235  ennnfonelemr  11972  ctinf  11979