Theorem eqtr2 2754

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 2737	. 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 2705

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

This theorem is referenced by:  eqvincg  3599  reusv3i  5346  moop2  5447  relopabi  5768  relop  5796  f0rn0  6716  fliftfun  7255  soseq  8098  addlsub  11544  wrd2ind  14637  fsum2dlem  15684  fprodser  15863  0dvds  16194  cncongr1  16585  4sqlem12  16875  cshwshashlem1  17014  catideu  17589  pj1eu  19616  lspsneu  21069  1marepvmarrepid  22510  mdetunilem6  22552  qtopeu  23651  qtophmeo  23752  dscmet  24507  isosctrlem2  26776  ppiub  27162  sltsolem1  27634  nolt02o  27654  nogt01o  27655  axcgrtr  28914  axeuclid  28962  axcontlem2  28964  uhgr2edg  29207  usgredgreu  29217  uspgredg2vtxeu  29219  wlkon2n0  29664  spthonepeq  29751  usgr2wlkneq  29755  2pthon3v  29942  umgr2adedgspth  29947  clwwlknondisj  30112  frgr2wwlkeqm  30332  2wspmdisj  30338  ajmoi  30859  chocunii  31302  3oalem2  31664  adjmo  31833  cdjreui  32433  eqtrb  32474  probun  34504  bnj551  34826  fineqvnttrclselem1  35213  satfv0fun  35487  satffunlem  35517  satffunlem1lem1  35518  satffunlem2lem1  35520  r1peuqusdeg1  35759  btwnswapid  36133  bj-snsetex  37080  bj-bary1lem1  37428  poimirlem4  37737  exidu1  37969  rngoideu  38016  mapdpglem31  41875  grpods  42360  remul01  42577  frege55b  44054  frege55c  44075  cncfiooicclem1  46053  euoreqb  47271  isuspgrim0lem  48055  aacllem  49962