Theorem eqtr3t 1494

Description: A transitive law for class equality.

Assertion

Ref	Expression
eqtr3t	|- ((A = C /\ B = C) -> A = B)

Proof of Theorem eqtr3t

Step	Hyp	Ref	Expression
1		eqtrt 1492	. 2 |- ((A = C /\ C = B) -> A = B)
2		eqcom 1477	. 2 |- (B = C <-> C = B)
3	1, 2	sylan2b 452	1 |- ((A = C /\ B = C) -> A = B)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 956

This theorem is referenced by:  eueq 1916  preqsn 2486  reuunisn 2895  funsn 3543  funopg 3547  foco 3682  oawordeulem 4188  negeu 5355  xrlttrit 5552  receu 5701  grpinveu 8064  ringsn 8163  psrn 8650  5oalem4 9602  bra11 10041  imonclem 10741  ismonc 10742

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain