Theorem eqtr2 2759

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  eqvincg  3648  reusv3i  5410  moop2  5512  relopabi  5835  relop  5864  f0rn0  6794  fliftfun  7332  soseq  8183  addlsub  11677  wrd2ind  14758  fsum2dlem  15803  fprodser  15982  0dvds  16311  cncongr1  16701  4sqlem12  16990  cshwshashlem1  17130  catideu  17720  pj1eu  19729  lspsneu  21143  1marepvmarrepid  22597  mdetunilem6  22639  qtopeu  23740  qtophmeo  23841  dscmet  24601  isosctrlem2  26877  ppiub  27263  sltsolem1  27735  nolt02o  27755  nogt01o  27756  axcgrtr  28945  axeuclid  28993  axcontlem2  28995  uhgr2edg  29240  usgredgreu  29250  uspgredg2vtxeu  29252  wlkon2n0  29699  spthonepeq  29785  usgr2wlkneq  29789  2pthon3v  29973  umgr2adedgspth  29978  clwwlknondisj  30140  frgr2wwlkeqm  30360  2wspmdisj  30366  ajmoi  30887  chocunii  31330  3oalem2  31692  adjmo  31861  cdjreui  32461  eqtrb  32502  probun  34401  bnj551  34735  satfv0fun  35356  satffunlem  35386  satffunlem1lem1  35387  satffunlem2lem1  35389  r1peuqusdeg1  35628  btwnswapid  35999  bj-snsetex  36946  bj-bary1lem1  37294  poimirlem4  37611  exidu1  37843  rngoideu  37890  mapdpglem31  41686  grpods  42176  remul01  42414  frege55b  43887  frege55c  43908  cncfiooicclem1  45849  euoreqb  47059  isuspgrim0lem  47809  aacllem  49032