Theorem equequ1 1735

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 1527	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1732	. 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 1472  ax-ie2 1517  ax-8 1527  ax-17 1549  ax-i9 1553

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1782  drsb1  1822  equsb3lem  1978  euequ1  2149  axext3  2188  cbvreuvw  2744  reu6  2962  reu7  2968  disjiun  4039  cbviota  5237  dff13f  5839  poxp  6318  dcdifsnid  6590  supmoti  7095  isoti  7109  nninfwlpoim  7281  exmidontriimlem3  7335  exmidontriim  7337  netap  7366  fsum2dlemstep  11745  ennnfonelemr  12794  ctinf  12801  reap0  15997