Theorem equequ1 1723

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 1515	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1720	. 2 |- ( x = y -> ( y = z -> x = z ) )
3	1, 2	impbid 129	1 |- ( x = y -> ( x = z <-> y = z ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1770  drsb1  1810  equsb3lem  1962  euequ1  2133  axext3  2172  cbvreuvw  2724  reu6  2941  reu7  2947  disjiun  4016  cbviota  5204  dff13f  5795  poxp  6261  dcdifsnid  6533  supmoti  7026  isoti  7040  nninfwlpoim  7211  exmidontriimlem3  7257  exmidontriim  7259  netap  7288  fsum2dlemstep  11483  ennnfonelemr  12485  ctinf  12492  reap0  15294