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  5361  moop2  5464  relopabi  5787  relop  5816  f0rn0  6747  fliftfun  7289  soseq  8140  addlsub  11600  wrd2ind  14694  fsum2dlem  15742  fprodser  15921  0dvds  16252  cncongr1  16643  4sqlem12  16933  cshwshashlem1  17072  catideu  17642  pj1eu  19632  lspsneu  21039  1marepvmarrepid  22468  mdetunilem6  22510  qtopeu  23609  qtophmeo  23710  dscmet  24466  isosctrlem2  26735  ppiub  27121  sltsolem1  27593  nolt02o  27613  nogt01o  27614  axcgrtr  28848  axeuclid  28896  axcontlem2  28898  uhgr2edg  29141  usgredgreu  29151  uspgredg2vtxeu  29153  wlkon2n0  29600  spthonepeq  29688  usgr2wlkneq  29692  2pthon3v  29879  umgr2adedgspth  29884  clwwlknondisj  30046  frgr2wwlkeqm  30266  2wspmdisj  30272  ajmoi  30793  chocunii  31236  3oalem2  31598  adjmo  31767  cdjreui  32367  eqtrb  32409  probun  34416  bnj551  34738  satfv0fun  35358  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  r1peuqusdeg1  35630  btwnswapid  36000  bj-snsetex  36946  bj-bary1lem1  37294  poimirlem4  37613  exidu1  37845  rngoideu  37892  mapdpglem31  41692  grpods  42177  remul01  42390  frege55b  43879  frege55c  43900  cncfiooicclem1  45884  euoreqb  47100  isuspgrim0lem  47883  aacllem  49780