Theorem eqtr2 2491

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 2478	. 2 |- ( A = B <-> B = A )
2		eqtr 2490	. 2 |- ( ( B = A /\ A = C ) -> B = C )
3	1, 2	sylanb 480	1 |- ( ( A = B /\ A = C ) -> B = C )

Syntax hints:   -> wi 4   /\ wa 376   = wceq 1452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-cleq 2464

This theorem is referenced by:  eqvinc  3154  reusv3i  4608  moop2  4696  relop  4990  restidsing  5167  f0rn0  5781  fliftfun  6223  addlsub  10057  wrd2ind  12888  fsum2dlem  13908  fprodser  14080  0dvds  14400  4sqlem12  14979  cshwshashlem1  15144  catideu  15659  pj1eu  17424  lspsneu  18424  1marepvmarrepid  19677  mdetunilem6  19719  qtopeu  20808  qtophmeo  20909  dscmet  21665  isosctrlem2  23827  ppiub  24211  axcgrtr  25024  axeuclid  25072  axcontlem2  25074  usgraedgprv  25182  usgra2edg  25188  usgraedgreu  25194  spthonepeq  25396  wlkdvspthlem  25416  usgra2wlkspthlem1  25426  el2wlkonotot0  25679  2spotdisj  25868  numclwwlkdisj  25887  exidu1  26135  rngoideu  26193  ajmoi  26581  chocunii  27035  3oalem2  27397  adjmo  27566  cdjreui  28166  eqvincg  28189  probun  29325  bnj551  29624  soseq  30563  sltsolem1  30628  btwnswapid  30855  bj-snsetex  31627  bj-bary1lem1  31786  poimirlem4  32008  mapdpglem31  35342  frege55b  36564  frege55c  36585  cncfiooicclem1  37868  uhgr2edg  39453  usgredgreu  39459  uspgredg2vtxeu  39461  spthonepeq-av  39944  usgr2wlkneq  39948  2pthon3v-av  40065  umgr2adedgspth  40070  usgvincvadeu  40225  usgvincvadeuALT  40228  aacllem  41046