Theorem equequ1 1130

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 961	. 2 |- (x = y -> (x = z -> y = z))
2		equtr 1127	. 2 |- (x = y -> (y = z -> x = z))
3	1, 2	impbid 514	1 |- (x = y -> (x = z <-> y = z))

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

This theorem is referenced by:  drsb1 1171  hbsb4 1243  equsb3lem 1324  sb7f 1336  dveeq1 1348  ax11eq 1356  a12lem1 1369  sb8eu 1383  2mo 1440  2eu6 1447  zfext2 1454  aceq0 4702  axac 4717  axrepndlem1 4916  axpowndlem2 4922  axacndlem5 4935  zfcndac 4943  ghomf1olem 10301

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-8 961  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

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

Copyright terms: Public domain