Theorem equequ1 1134

Description: An equivalence law for equality.

Assertion

Ref	Expression
equequ1	|- (x = y -> (x = z <-> y = z))

Proof of Theorem equequ1

Step	Hyp	Ref	Expression
1		ax-8 964	. 2 |- (x = y -> (x = z -> y = z))
2		equtr 1131	. 2 |- (x = y -> (y = z -> x = z))
3	1, 2	impbid 516	1 |- (x = y -> (x = z <-> y = z))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956

This theorem is referenced by:  drsb1 1175  hbsb4 1248  equsb3lem 1329  sb7f 1341  dveeq1 1354  dveeq1ALT 1355  ax11eq 1363  a12lem1 1376  sb8eu 1390  2mo 1447  2eu6 1454  zfext2 1461  aceq0 4730  axac 4745  axrepndlem1 4944  axpowndlem2 4950  axacndlem5 4963  zfcndac 4971  ghomf1olem 10396

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-8 964  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain