Theorem eqtr2 2756

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  eqvincg  3635  reusv3i  5401  moop2  5501  relopabi  5820  relop  5848  f0rn0  6773  fliftfun  7305  soseq  8141  addlsub  11626  wrd2ind  14669  fsum2dlem  15712  fprodser  15889  0dvds  16216  cncongr1  16600  4sqlem12  16885  cshwshashlem1  17025  catideu  17615  pj1eu  19558  lspsneu  20728  1marepvmarrepid  22068  mdetunilem6  22110  qtopeu  23211  qtophmeo  23312  dscmet  24072  isosctrlem2  26313  ppiub  26696  sltsolem1  27167  nolt02o  27187  nogt01o  27188  axcgrtr  28162  axeuclid  28210  axcontlem2  28212  uhgr2edg  28454  usgredgreu  28464  uspgredg2vtxeu  28466  wlkon2n0  28912  spthonepeq  28998  usgr2wlkneq  29002  2pthon3v  29186  umgr2adedgspth  29191  clwwlknondisj  29353  frgr2wwlkeqm  29573  2wspmdisj  29579  ajmoi  30098  chocunii  30541  3oalem2  30903  adjmo  31072  cdjreui  31672  eqtrb  31701  probun  33406  bnj551  33741  satfv0fun  34350  satffunlem  34380  satffunlem1lem1  34381  satffunlem2lem1  34383  btwnswapid  34977  bj-snsetex  35832  bj-bary1lem1  36180  poimirlem4  36480  exidu1  36712  rngoideu  36759  mapdpglem31  40562  remul01  41276  frege55b  42633  frege55c  42654  cncfiooicclem1  44595  euoreqb  45803  aacllem  47801