Theorem eqtr2 2757

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 2740	. 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 2123  ax-ext 2708

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

This theorem is referenced by:  eqvincg  3602  reusv3i  5349  moop2  5450  relopabi  5771  relop  5799  f0rn0  6719  fliftfun  7258  soseq  8101  addlsub  11553  wrd2ind  14646  fsum2dlem  15693  fprodser  15872  0dvds  16203  cncongr1  16594  4sqlem12  16884  cshwshashlem1  17023  catideu  17598  pj1eu  19625  lspsneu  21078  1marepvmarrepid  22519  mdetunilem6  22561  qtopeu  23660  qtophmeo  23761  dscmet  24516  isosctrlem2  26785  ppiub  27171  ltssolem1  27643  nolt02o  27663  nogt01o  27664  axcgrtr  28988  axeuclid  29036  axcontlem2  29038  uhgr2edg  29281  usgredgreu  29291  uspgredg2vtxeu  29293  wlkon2n0  29738  spthonepeq  29825  usgr2wlkneq  29829  2pthon3v  30016  umgr2adedgspth  30021  clwwlknondisj  30186  frgr2wwlkeqm  30406  2wspmdisj  30412  ajmoi  30933  chocunii  31376  3oalem2  31738  adjmo  31907  cdjreui  32507  eqtrb  32548  probun  34576  bnj551  34898  fineqvnttrclselem1  35277  satfv0fun  35565  satffunlem  35595  satffunlem1lem1  35596  satffunlem2lem1  35598  r1peuqusdeg1  35837  btwnswapid  36211  bj-snsetex  37164  bj-bary1lem1  37516  poimirlem4  37825  exidu1  38057  rngoideu  38104  mapdpglem31  41963  grpods  42448  remul01  42662  frege55b  44138  frege55c  44159  cncfiooicclem1  46137  euoreqb  47355  isuspgrim0lem  48139  aacllem  50046