Theorem eqtr2 2429

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 2411	. 2 |- ( A = B <-> B = A )
2		eqtr 2428	. 2 |- ( ( B = A /\ A = C ) -> B = C )
3	1, 2	sylanb 470	1 |- ( ( A = B /\ A = C ) -> B = C )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2394

This theorem is referenced by:  eqvinc  3176  reusv3i  4601  moop2  4685  relop  4974  restidsing  5150  f0rn0  5753  fliftfun  6193  addlsub  10019  wrd2ind  12759  fsum2dlem  13736  fprodser  13908  0dvds  14213  4sqlem12  14683  cshwshashlem1  14789  catideu  15289  pj1eu  17038  lspsneu  18089  1marepvmarrepid  19369  mdetunilem6  19411  qtopeu  20509  qtophmeo  20610  dscmet  21385  isosctrlem2  23478  ppiub  23860  axcgrtr  24635  axeuclid  24683  axcontlem2  24685  usgraedgprv  24793  usgra2edg  24799  usgraedgreu  24805  spthonepeq  25006  wlkdvspthlem  25026  usgra2wlkspthlem1  25036  el2wlkonotot0  25289  2spotdisj  25478  numclwwlkdisj  25497  exidu1  25742  rngoideu  25800  ajmoi  26188  chocunii  26633  3oalem2  26995  adjmo  27164  cdjreui  27764  eqvincg  27787  probun  28864  bnj551  29126  soseq  30065  sltsolem1  30128  btwnswapid  30355  bj-snsetex  31086  bj-bary1lem1  31241  mapdpglem31  34723  frege55b  35878  frege55c  35899  cncfiooicclem1  37064  usgvincvadeu  38034  usgvincvadeuALT  38037  aacllem  38860