Theorem equequ1 1760

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 1553	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1757	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1807  drsb1  1847  equsb3lem  2003  euequ1  2175  axext3  2214  cbvreuvw  2774  reu6  2996  reu7  3002  reu8nf  3114  disjiun  4088  cbviota  5298  dff13f  5921  poxp  6406  dcdifsnid  6715  modom  7037  supmoti  7235  isoti  7249  nninfwlpoim  7421  exmidontriimlem3  7481  exmidontriim  7483  netap  7516  fsum2dlemstep  12058  ennnfonelemr  13107  ctinf  13114  reap0  16774