Theorem eqtr2 2751

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqvincg  3617  reusv3i  5362  moop2  5465  relopabi  5788  relop  5817  f0rn0  6748  fliftfun  7290  soseq  8141  addlsub  11601  wrd2ind  14695  fsum2dlem  15743  fprodser  15922  0dvds  16253  cncongr1  16644  4sqlem12  16934  cshwshashlem1  17073  catideu  17643  pj1eu  19633  lspsneu  21040  1marepvmarrepid  22469  mdetunilem6  22511  qtopeu  23610  qtophmeo  23711  dscmet  24467  isosctrlem2  26736  ppiub  27122  sltsolem1  27594  nolt02o  27614  nogt01o  27615  axcgrtr  28849  axeuclid  28897  axcontlem2  28899  uhgr2edg  29142  usgredgreu  29152  uspgredg2vtxeu  29154  wlkon2n0  29601  spthonepeq  29689  usgr2wlkneq  29693  2pthon3v  29880  umgr2adedgspth  29885  clwwlknondisj  30047  frgr2wwlkeqm  30267  2wspmdisj  30273  ajmoi  30794  chocunii  31237  3oalem2  31599  adjmo  31768  cdjreui  32368  eqtrb  32410  probun  34417  bnj551  34739  satfv0fun  35365  satffunlem  35395  satffunlem1lem1  35396  satffunlem2lem1  35398  r1peuqusdeg1  35637  btwnswapid  36012  bj-snsetex  36958  bj-bary1lem1  37306  poimirlem4  37625  exidu1  37857  rngoideu  37904  mapdpglem31  41704  grpods  42189  remul01  42402  frege55b  43893  frege55c  43914  cncfiooicclem1  45898  euoreqb  47114  isuspgrim0lem  47897  aacllem  49794