Theorem eqtr2 2461

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof 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		eqcom 2445	. 2 |- ( A = B <-> B = A )
2		eqtr 2460	. 2 |- ( ( B = A /\ A = C ) -> B = C )
3	1, 2	sylanb 472	1 |- ( ( A = B /\ A = C ) -> B = C )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436

This theorem is referenced by:  eqvinc  3086  reusv3i  4499  moop2  4586  relop  4990  restidsing  5162  fliftfun  6005  th3qlem1  7206  wrd2ind  12372  fsum2dlem  13237  0dvds  13553  4sqlem12  14017  cshwshashlem1  14122  catideu  14613  pj1eu  16193  lspsneu  17204  1marepvmarrepid  18386  mdetunilem6  18423  bwthOLD  19014  qtopeu  19289  qtophmeo  19390  dscmet  20165  isosctrlem2  22217  ppiub  22543  axcgrtr  23161  axeuclid  23209  axcontlem2  23211  usgraedgprv  23295  usgra2edg  23301  usgraedgreu  23306  spthonepeq  23486  wlkdvspthlem  23506  exidu1  23813  rngoideu  23871  ajmoi  24259  chocunii  24704  3oalem2  25066  adjmo  25236  cdjreui  25836  eqvincg  25859  probun  26802  fprodser  27462  soseq  27715  sltsolem1  27809  btwnswapid  28048  f0rn0  30141  usgra2wlkspthlem1  30296  el2wlkonotot0  30391  2spotdisj  30654  numclwwlkdisj  30673  bnj551  31734  bj-snsetex  32456  bj-lsub  32591  bj-bary1lem1  32600  mapdpglem31  35348