Theorem eqtr2 2752

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)

Assertion

Ref	Expression
eqtr2	⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqeq1 2735	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpa 476	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqvincg  3598  reusv3i  5337  moop2  5437  relopabi  5757  relop  5785  f0rn0  6703  fliftfun  7241  soseq  8084  addlsub  11528  wrd2ind  14625  fsum2dlem  15672  fprodser  15851  0dvds  16182  cncongr1  16573  4sqlem12  16863  cshwshashlem1  17002  catideu  17576  pj1eu  19603  lspsneu  21055  1marepvmarrepid  22485  mdetunilem6  22527  qtopeu  23626  qtophmeo  23727  dscmet  24482  isosctrlem2  26751  ppiub  27137  sltsolem1  27609  nolt02o  27629  nogt01o  27630  axcgrtr  28888  axeuclid  28936  axcontlem2  28938  uhgr2edg  29181  usgredgreu  29191  uspgredg2vtxeu  29193  wlkon2n0  29638  spthonepeq  29725  usgr2wlkneq  29729  2pthon3v  29916  umgr2adedgspth  29921  clwwlknondisj  30083  frgr2wwlkeqm  30303  2wspmdisj  30309  ajmoi  30830  chocunii  31273  3oalem2  31635  adjmo  31804  cdjreui  32404  eqtrb  32445  probun  34424  bnj551  34746  fineqvnttrclselem1  35133  satfv0fun  35407  satffunlem  35437  satffunlem1lem1  35438  satffunlem2lem1  35440  r1peuqusdeg1  35679  btwnswapid  36051  bj-snsetex  36997  bj-bary1lem1  37345  poimirlem4  37664  exidu1  37896  rngoideu  37943  mapdpglem31  41742  grpods  42227  remul01  42440  frege55b  43930  frege55c  43951  cncfiooicclem1  45931  euoreqb  47140  isuspgrim0lem  47924  aacllem  49833