Theorem equequ1 1712

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 1504	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1709	. 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 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1759  drsb1  1799  equsb3lem  1950  euequ1  2121  axext3  2160  cbvreuvw  2709  reu6  2926  reu7  2932  disjiun  3996  cbviota  5180  dff13f  5766  poxp  6228  dcdifsnid  6500  supmoti  6987  isoti  7001  nninfwlpoim  7171  exmidontriimlem3  7217  exmidontriim  7219  netap  7248  fsum2dlemstep  11433  ennnfonelemr  12414  ctinf  12421  reap0  14577