Theorem eqtr2 2487

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 2469	. 2 |- ( A = B <-> B = A )
2		eqtr 2486	. 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 1374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2452

This theorem is referenced by:  eqvinc  3223  reusv3i  4647  moop2  4735  relop  5144  restidsing  5321  f0rn0  5761  fliftfun  6189  wrd2ind  12653  fsum2dlem  13534  0dvds  13854  4sqlem12  14322  cshwshashlem1  14427  catideu  14919  pj1eu  16503  lspsneu  17545  1marepvmarrepid  18837  mdetunilem6  18879  bwthOLD  19670  qtopeu  19945  qtophmeo  20046  dscmet  20821  isosctrlem2  22874  ppiub  23200  axcgrtr  23887  axeuclid  23935  axcontlem2  23937  usgraedgprv  24038  usgra2edg  24044  usgraedgreu  24050  spthonepeq  24251  wlkdvspthlem  24271  usgra2wlkspthlem1  24281  el2wlkonotot0  24534  2spotdisj  24724  numclwwlkdisj  24743  exidu1  24990  rngoideu  25048  ajmoi  25436  chocunii  25881  3oalem2  26243  adjmo  26413  cdjreui  27013  eqvincg  27036  probun  27984  fprodser  28644  soseq  28897  sltsolem1  28991  btwnswapid  29230  cncfiooicclem1  31187  usgvincvadeu  31807  usgvincvadeuALT  31810  bnj551  32753  bj-snsetex  33477  bj-lsub  33618  bj-bary1lem1  33627  mapdpglem31  36375  frege55b  36764  frege55c  36785