Theorem eqtr2 2750

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 2733	. 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 2701

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

This theorem is referenced by:  eqvincg  3614  reusv3i  5359  moop2  5462  relopabi  5785  relop  5814  f0rn0  6745  fliftfun  7287  soseq  8138  addlsub  11594  wrd2ind  14688  fsum2dlem  15736  fprodser  15915  0dvds  16246  cncongr1  16637  4sqlem12  16927  cshwshashlem1  17066  catideu  17636  pj1eu  19626  lspsneu  21033  1marepvmarrepid  22462  mdetunilem6  22504  qtopeu  23603  qtophmeo  23704  dscmet  24460  isosctrlem2  26729  ppiub  27115  sltsolem1  27587  nolt02o  27607  nogt01o  27608  axcgrtr  28842  axeuclid  28890  axcontlem2  28892  uhgr2edg  29135  usgredgreu  29145  uspgredg2vtxeu  29147  wlkon2n0  29594  spthonepeq  29682  usgr2wlkneq  29686  2pthon3v  29873  umgr2adedgspth  29878  clwwlknondisj  30040  frgr2wwlkeqm  30260  2wspmdisj  30266  ajmoi  30787  chocunii  31230  3oalem2  31592  adjmo  31761  cdjreui  32361  eqtrb  32403  probun  34410  bnj551  34732  satfv0fun  35358  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  r1peuqusdeg1  35630  btwnswapid  36005  bj-snsetex  36951  bj-bary1lem1  37299  poimirlem4  37618  exidu1  37850  rngoideu  37897  mapdpglem31  41697  grpods  42182  remul01  42395  frege55b  43886  frege55c  43907  cncfiooicclem1  45891  euoreqb  47110  isuspgrim0lem  47893  aacllem  49790