Theorem equequ1 1734

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 1526	. 2 |- ( x = y -> ( x = z -> y = z ) )
2		equtr 1731	. 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 1471  ax-ie2 1516  ax-8 1526  ax-17 1548  ax-i9 1552

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1781  drsb1  1821  equsb3lem  1977  euequ1  2148  axext3  2187  cbvreuvw  2743  reu6  2961  reu7  2967  disjiun  4038  cbviota  5236  dff13f  5838  poxp  6317  dcdifsnid  6589  supmoti  7094  isoti  7108  nninfwlpoim  7280  exmidontriimlem3  7334  exmidontriim  7336  netap  7365  fsum2dlemstep  11687  ennnfonelemr  12736  ctinf  12743  reap0  15930