Theorem eqtr2 1905

Description: A transitive law for class equality. (The proof was shortened by Andrew Salmon, 25-May-2011.)

Assertion

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

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqtr 1904	. 2 |- ((B = A /\ A = C) -> B = C)
2		eqcom 1886	. 2 |- (A = B <-> B = A)
3	1, 2	sylanb 498	1 |- ((A = B /\ A = C) -> B = C)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298

This theorem is referenced by:  eqvinc 2387  csbie2t 2578  moop2 3548  eufromeq2 3829  eufromeq6 3833  relop 4113  th3qlem1 5373  aceq5lem4 5900  creur 7992  creui 7993  replim 8011  ringideu 9470  ajmoi 9860  chocunii 10805  3oalem2 11243  adjmo 11395  adjvalval 11498  cdjreui 12004  bnj551 12537  0dvds 13675  soseq 13955  axsltsolem1 14006  axfelem15 14045  fnbigcup 14075  restidsing 14391  prj1 14395  bwt2 14960  topgrpbs 14974  filssufillem 15570  filcon 15580  limfilcf 15587  uffclsflim 15616  filnetlem4 15643  filnetlem5 15644  eropreu 15733  heiborlem10 15964  ringideuNEW 17146

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain