Theorem eqtr2 2786

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  eqvincg  3609  reusv3i  5377  moop2  5487  relopabi  5811  relop  5838  f0rn0  6767  fliftfun  7319  soseq  8161  addlsub  11645  wrd2ind  14782  fsum2dlem  15844  fprodser  16026  0dvds  16356  cncongr1  16747  4sqlem12  17038  cshwshashlem1  17177  catideu  17753  pj1eu  19810  lspsneu  21297  1marepvmarrepid  22782  mdetunilem6  22824  qtopeu  23924  qtophmeo  24025  dscmet  24780  isosctrlem2  27035  ppiub  27419  ltssolem1  27890  nolt02o  27910  nogt01o  27911  axcgrtr  29320  axeuclid  29368  axcontlem2  29370  uhgr2edg  29616  usgredgreu  29626  uspgredg2vtxeu  29628  wlkon2n0  30072  spthonepeq  30165  usgr2wlkneq  30169  2pthon3v  30359  umgr2adedgspth  30364  clwwlknondisj  30529  frgr2wwlkeqm  30753  2wspmdisj  30759  ajmoi  31281  chocunii  31724  3oalem2  32086  adjmo  32255  cdjreui  32855  eqtrb  32891  probun  34874  bnj551  35196  fineqvnttrclselem1  35591  satfv0fun  35900  satffunlem  35930  satffunlem1lem1  35931  satffunlem2lem1  35933  r1peuqusdeg1  36172  btwnswapid  36546  bj-snsetex  37656  bj-bary1lem1  38012  poimirlem4  38332  exidu1  38565  rngoideu  38612  disjimrmoeqec  39515  mapdpglem31  42535  grpods  43019  remul01  43226  frege55b  44681  frege55c  44702  cncfiooicclem1  46665  euoreqb  47904  isuspgrim0lem  48716  aacllem  50678