Theorem eqtr2 2630

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603

This theorem is referenced by:  eqvinc  3300  reusv3i  4801  moop2  4891  relopabi  5167  relop  5194  restidsingOLD  5378  f0rn0  6003  fliftfun  6462  addlsub  10326  wrd2ind  13329  fsum2dlem  14343  fprodser  14518  0dvds  14840  cncongr1  15219  4sqlem12  15498  cshwshashlem1  15640  catideu  16159  pj1eu  17932  lspsneu  18944  1marepvmarrepid  20200  mdetunilem6  20242  qtopeu  21329  qtophmeo  21430  dscmet  22187  isosctrlem2  24349  ppiub  24729  axcgrtr  25595  axeuclid  25643  axcontlem2  25645  usgraedgprv  25905  usgra2edg  25911  usgraedgreu  25917  spthonepeq  26117  wlkdvspthlem  26137  usgra2wlkspthlem1  26147  el2wlkonotot0  26399  2spotdisj  26588  numclwwlkdisj  26607  ajmoi  27098  chocunii  27544  3oalem2  27906  adjmo  28075  cdjreui  28675  eqvincg  28698  probun  29808  bnj551  30066  soseq  30995  sltsolem1  31067  btwnswapid  31294  bj-snsetex  32144  bj-bary1lem1  32338  poimirlem4  32583  exidu1  32825  rngoideu  32872  mapdpglem31  36010  frege55b  37211  frege55c  37232  cncfiooicclem1  38779  uhgr2edg  40435  usgredgreu  40445  uspgredg2vtxeu  40447  wlkOn2n0  40874  spthonepeq-av  40958  usgr2wlkneq  40962  2pthon3v-av  41150  umgr2adedgspth  41155  clwwlksndisj  41280  2wspmdisj  41501  aacllem  42356