Theorem equequ1 1705

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 1497	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1702	. 2 |- ( x = y -> ( y = z -> x = z ) )
3	1, 2	impbid 128	1 |- ( x = y -> ( x = z <-> y = z ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equveli  1752  drsb1  1792  equsb3lem  1943  euequ1  2114  axext3  2153  cbvreuvw  2702  reu6  2919  reu7  2925  disjiun  3982  cbviota  5163  dff13f  5747  poxp  6209  dcdifsnid  6481  supmoti  6968  isoti  6982  exmidontriimlem3  7193  exmidontriim  7195  fsum2dlemstep  11390  ennnfonelemr  12371  ctinf  12378  reap0  14055