Theorem eqtr2 2790

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 2773	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpa 481	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqvincg  3616  reusv3i  5376  moop2  5486  relopabi  5810  relop  5837  f0rn0  6764  fliftfun  7311  soseq  8155  addlsub  11630  wrd2ind  14760  fsum2dlem  15821  fprodser  16003  0dvds  16334  cncongr1  16725  4sqlem12  17016  cshwshashlem1  17155  catideu  17731  pj1eu  19766  lspsneu  21225  1marepvmarrepid  22701  mdetunilem6  22743  qtopeu  23842  qtophmeo  23943  dscmet  24698  isosctrlem2  26950  ppiub  27334  ltssolem1  27805  nolt02o  27825  nogt01o  27826  axcgrtr  29206  axeuclid  29254  axcontlem2  29256  uhgr2edg  29499  usgredgreu  29509  uspgredg2vtxeu  29511  wlkon2n0  29955  spthonepeq  30042  usgr2wlkneq  30046  2pthon3v  30233  umgr2adedgspth  30238  clwwlknondisj  30403  frgr2wwlkeqm  30623  2wspmdisj  30629  ajmoi  31151  chocunii  31594  3oalem2  31956  adjmo  32125  cdjreui  32725  eqtrb  32761  probun  34754  bnj551  35076  fineqvnttrclselem1  35467  satfv0fun  35796  satffunlem  35826  satffunlem1lem1  35827  satffunlem2lem1  35829  r1peuqusdeg1  36068  btwnswapid  36442  bj-snsetex  37521  bj-bary1lem1  37877  poimirlem4  38197  exidu1  38429  rngoideu  38476  disjimrmoeqec  39381  mapdpglem31  42401  grpods  42885  remul01  43092  frege55b  44549  frege55c  44570  cncfiooicclem1  46533  euoreqb  47769  isuspgrim0lem  48581  aacllem  50509