Theorem equequ1 1121

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 1101	. 2 |- (x = y -> (x = z -> y = z))
2		equtr 1118	. 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 1099

This theorem is referenced by:  drsb1 1158  hbsb4 1232  equsb3lem 1311  sb7f 1323  dveeq1 1335  ax11eq 1340  a12lem1 1353  sb8eu 1367  2mo 1424  2eu6 1431  zfext2 1438  aceq0 4654  axac 4669  axrepndlem1 4867  axpowndlem2 4873  axacndlem5 4886  zfcndac 4894  ghomf1olem 8663

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-8 1101  ax-9 1102  ax-12 1104

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

Copyright terms: Public domain