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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718

This theorem is referenced by:  eqvincg  3632  reusv3i  5400  moop2  5500  relopabi  5820  relop  5849  f0rn0  6779  fliftfun  7316  soseq  8165  addlsub  11671  wrd2ind  14726  fsum2dlem  15769  fprodser  15946  0dvds  16274  cncongr1  16663  4sqlem12  16953  cshwshashlem1  17093  catideu  17683  pj1eu  19690  lspsneu  21100  1marepvmarrepid  22565  mdetunilem6  22607  qtopeu  23708  qtophmeo  23809  dscmet  24569  isosctrlem2  26844  ppiub  27230  sltsolem1  27702  nolt02o  27722  nogt01o  27723  axcgrtr  28846  axeuclid  28894  axcontlem2  28896  uhgr2edg  29141  usgredgreu  29151  uspgredg2vtxeu  29153  wlkon2n0  29600  spthonepeq  29686  usgr2wlkneq  29690  2pthon3v  29874  umgr2adedgspth  29879  clwwlknondisj  30041  frgr2wwlkeqm  30261  2wspmdisj  30267  ajmoi  30788  chocunii  31231  3oalem2  31593  adjmo  31762  cdjreui  32362  eqtrb  32399  probun  34266  bnj551  34600  satfv0fun  35212  satffunlem  35242  satffunlem1lem1  35243  satffunlem2lem1  35245  r1peuqusdeg1  35484  btwnswapid  35854  bj-snsetex  36683  bj-bary1lem1  37031  poimirlem4  37338  exidu1  37570  rngoideu  37617  mapdpglem31  41415  grpods  41906  remul01  42118  frege55b  43601  frege55c  43622  cncfiooicclem1  45550  euoreqb  46758  isuspgrim0lem  47486  aacllem  48585