Theorem eqtr2 2450

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 2432	. 2 |- ( A = B <-> B = A )
2		eqtr 2449	. 2 |- ( ( B = A /\ A = C ) -> B = C )
3	1, 2	sylanb 475	1 |- ( ( A = B /\ A = C ) -> B = C )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-cleq 2415

This theorem is referenced by:  eqvinc  3199  reusv3i  4629  moop2  4713  relop  5002  restidsing  5178  f0rn0  5783  fliftfun  6218  addlsub  10040  wrd2ind  12830  fsum2dlem  13824  fprodser  13996  0dvds  14316  4sqlem12  14893  cshwshashlem1  15059  catideu  15574  pj1eu  17339  lspsneu  18339  1marepvmarrepid  19592  mdetunilem6  19634  qtopeu  20723  qtophmeo  20824  dscmet  21579  isosctrlem2  23740  ppiub  24124  axcgrtr  24937  axeuclid  24985  axcontlem2  24987  usgraedgprv  25095  usgra2edg  25101  usgraedgreu  25107  spthonepeq  25309  wlkdvspthlem  25329  usgra2wlkspthlem1  25339  el2wlkonotot0  25592  2spotdisj  25781  numclwwlkdisj  25800  exidu1  26046  rngoideu  26104  ajmoi  26492  chocunii  26946  3oalem2  27308  adjmo  27477  cdjreui  28077  eqvincg  28100  probun  29254  bnj551  29554  soseq  30493  sltsolem1  30556  btwnswapid  30783  bj-snsetex  31519  bj-bary1lem1  31674  poimirlem4  31902  mapdpglem31  35234  frege55b  36395  frege55c  36416  cncfiooicclem1  37635  usgr2edg  38954  usgredgreu  38960  usgredg2vtxeu  38962  usgvincvadeu  39059  usgvincvadeuALT  39062  aacllem  39884