Theorem equequ1 1132

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 962	. 2 ⊢ (x = y → (x = z → y = z))
2		equtr 1129	. 2 ⊢ (x = y → (y = z → x = z))
3	1, 2	impbid 515	1 ⊢ (x = y → (x = z ↔ y = z))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 954

This theorem is referenced by:  drsb1 1173  hbsb4 1246  equsb3lem 1327  sb7f 1339  dveeq1 1352  dveeq1ALT 1353  ax11eq 1361  a12lem1 1374  sb8eu 1388  2mo 1445  2eu6 1452  zfext2 1459  aceq0 4710  axac 4725  axrepndlem1 4924  axpowndlem2 4930  axacndlem5 4943  zfcndac 4951  ghomf1olem 10330

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-8 962  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

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

Copyright terms: Public domain