Theorem eqtr2 2760

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqvincg  3586  reusv3i  5333  moop2  5443  relopabi  5765  relop  5792  f0rn0  6712  fliftfun  7256  soseq  8099  addlsub  11557  wrd2ind  14676  fsum2dlem  15723  fprodser  15905  0dvds  16236  cncongr1  16627  4sqlem12  16918  cshwshashlem1  17057  catideu  17632  pj1eu  19662  lspsneu  21116  1marepvmarrepid  22558  mdetunilem6  22600  qtopeu  23699  qtophmeo  23800  dscmet  24555  isosctrlem2  26801  ppiub  27185  ltssolem1  27657  nolt02o  27677  nogt01o  27678  axcgrtr  29002  axeuclid  29050  axcontlem2  29052  uhgr2edg  29295  usgredgreu  29305  uspgredg2vtxeu  29307  wlkon2n0  29751  spthonepeq  29838  usgr2wlkneq  29842  2pthon3v  30029  umgr2adedgspth  30034  clwwlknondisj  30199  frgr2wwlkeqm  30419  2wspmdisj  30425  ajmoi  30947  chocunii  31390  3oalem2  31752  adjmo  31921  cdjreui  32521  eqtrb  32561  probun  34603  bnj551  34925  fineqvnttrclselem1  35302  satfv0fun  35599  satffunlem  35629  satffunlem1lem1  35630  satffunlem2lem1  35632  r1peuqusdeg1  35871  btwnswapid  36245  bj-snsetex  37316  bj-bary1lem1  37671  poimirlem4  37991  exidu1  38223  rngoideu  38270  disjimrmoeqec  39175  mapdpglem31  42195  grpods  42679  remul01  42884  frege55b  44341  frege55c  44362  cncfiooicclem1  46336  euoreqb  47572  isuspgrim0lem  48384  aacllem  50291