Theorem eqtr2 2484

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

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqcom 2466	. 2
2		eqtr 2483	. 2
3	1, 2	sylanb 472	1

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

This theorem is referenced by:  eqvinc  3226  reusv3i  4659  moop2  4747  relop  5158  restidsing  5335  f0rn0  5775  fliftfun  6210  wrd2ind  12703  fsum2dlem  13585  fprodser  13756  0dvds  14004  4sqlem12  14474  cshwshashlem1  14580  catideu  15072  pj1eu  16714  lspsneu  17769  1marepvmarrepid  19077  mdetunilem6  19119  bwthOLD  19911  qtopeu  20217  qtophmeo  20318  dscmet  21093  isosctrlem2  23153  ppiub  23479  axcgrtr  24218  axeuclid  24266  axcontlem2  24268  usgraedgprv  24376  usgra2edg  24382  usgraedgreu  24388  spthonepeq  24589  wlkdvspthlem  24609  usgra2wlkspthlem1  24619  el2wlkonotot0  24872  2spotdisj  25061  numclwwlkdisj  25080  exidu1  25328  rngoideu  25386  ajmoi  25774  chocunii  26219  3oalem2  26581  adjmo  26751  cdjreui  27351  eqvincg  27374  probun  28358  soseq  29334  sltsolem1  29428  btwnswapid  29667  cncfiooicclem1  31696  usgvincvadeu  32405  usgvincvadeuALT  32408  aacllem  33216  bnj551  33799  bj-snsetex  34521  bj-lsub  34671  bj-bary1lem1  34680  mapdpglem31  37430  frege55b  37924  frege55c  37945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

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