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 1552	. 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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1807  drsb1  1847  equsb3lem  2003  euequ1  2175  axext3  2214  cbvreuvw  2773  reu6  2995  reu7  3001  reu8nf  3113  disjiun  4083  cbviota  5291  dff13f  5910  poxp  6396  dcdifsnid  6671  modom  6993  supmoti  7191  isoti  7205  nninfwlpoim  7377  exmidontriimlem3  7437  exmidontriim  7439  netap  7472  fsum2dlemstep  11994  ennnfonelemr  13043  ctinf  13050  reap0  16662