Theorem eqtr2 2761

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 2741	. 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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqvincg  3648  reusv3i  5404  moop2  5507  relopabi  5832  relop  5861  f0rn0  6793  fliftfun  7332  soseq  8184  addlsub  11679  wrd2ind  14761  fsum2dlem  15806  fprodser  15985  0dvds  16314  cncongr1  16704  4sqlem12  16994  cshwshashlem1  17133  catideu  17718  pj1eu  19714  lspsneu  21125  1marepvmarrepid  22581  mdetunilem6  22623  qtopeu  23724  qtophmeo  23825  dscmet  24585  isosctrlem2  26862  ppiub  27248  sltsolem1  27720  nolt02o  27740  nogt01o  27741  axcgrtr  28930  axeuclid  28978  axcontlem2  28980  uhgr2edg  29225  usgredgreu  29235  uspgredg2vtxeu  29237  wlkon2n0  29684  spthonepeq  29772  usgr2wlkneq  29776  2pthon3v  29963  umgr2adedgspth  29968  clwwlknondisj  30130  frgr2wwlkeqm  30350  2wspmdisj  30356  ajmoi  30877  chocunii  31320  3oalem2  31682  adjmo  31851  cdjreui  32451  eqtrb  32493  probun  34421  bnj551  34756  satfv0fun  35376  satffunlem  35406  satffunlem1lem1  35407  satffunlem2lem1  35409  r1peuqusdeg1  35648  btwnswapid  36018  bj-snsetex  36964  bj-bary1lem1  37312  poimirlem4  37631  exidu1  37863  rngoideu  37910  mapdpglem31  41705  grpods  42195  remul01  42437  frege55b  43910  frege55c  43931  cncfiooicclem1  45908  euoreqb  47121  isuspgrim0lem  47871  aacllem  49320