Theorem eqtr2 2629

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 2616	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2		eqtr 2628	. 2 ⊢ ((𝐵 = 𝐴 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
3	1, 2	sylanb 487	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602

This theorem is referenced by:  eqvinc  3299  reusv3i  4795  moop2  4884  relop  5181  restidsingOLD  5364  f0rn0  5987  fliftfun  6439  addlsub  10298  wrd2ind  13277  fsum2dlem  14291  fprodser  14466  0dvds  14788  cncongr1  15167  4sqlem12  15446  cshwshashlem1  15588  catideu  16107  pj1eu  17880  lspsneu  18892  1marepvmarrepid  20147  mdetunilem6  20189  qtopeu  21276  qtophmeo  21377  dscmet  22134  isosctrlem2  24293  ppiub  24673  axcgrtr  25540  axeuclid  25588  axcontlem2  25590  usgraedgprv  25698  usgra2edg  25704  usgraedgreu  25710  spthonepeq  25910  wlkdvspthlem  25930  usgra2wlkspthlem1  25940  el2wlkonotot0  26192  2spotdisj  26381  numclwwlkdisj  26400  ajmoi  26891  chocunii  27337  3oalem2  27699  adjmo  27868  cdjreui  28468  eqvincg  28491  probun  29601  bnj551  29859  soseq  30788  sltsolem1  30860  btwnswapid  31087  bj-snsetex  31927  bj-bary1lem1  32121  poimirlem4  32366  exidu1  32608  rngoideu  32655  mapdpglem31  35793  frege55b  36994  frege55c  37015  cncfiooicclem1  38562  uhgr2edg  40416  usgredgreu  40426  uspgredg2vtxeu  40428  wlkOn2n0  40855  spthonepeq-av  40939  usgr2wlkneq  40943  2pthon3v-av  41131  umgr2adedgspth  41136  clwwlksndisj  41261  2wspmdisj  41482  aacllem  42298