Theorem equequ1 1736

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 1528	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1733	. 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 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1783  drsb1  1823  equsb3lem  1979  euequ1  2151  axext3  2190  cbvreuvw  2748  reu6  2969  reu7  2975  reu8nf  3087  disjiun  4054  cbviota  5256  dff13f  5862  poxp  6341  dcdifsnid  6613  supmoti  7121  isoti  7135  nninfwlpoim  7307  exmidontriimlem3  7366  exmidontriim  7368  netap  7401  fsum2dlemstep  11860  ennnfonelemr  12909  ctinf  12916  reap0  16199