Theorem eqtr2 2781

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  eqvincg  3601  reusv3i  5365  moop2  5473  relopabi  5800  relop  5828  f0rn0  6770  fliftfun  7322  soseq  8180  addlsub  11737  wrd2ind  14878  fsum2dlem  15943  fprodser  16123  0dvds  16453  cncongr1  16849  4sqlem12  17141  cshwshashlem1  17280  catideu  17856  pj1eu  19917  lspsneu  21408  1marepvmarrepid  22897  mdetunilem6  22939  qtopeu  24042  qtophmeo  24143  dscmet  24898  isosctrlem2  27154  ppiub  27538  ltssolem1  28039  nolt02o  28059  nogt01o  28060  axcgrtr  29500  axeuclid  29548  axcontlem2  29550  uhgr2edg  29796  usgredgreu  29806  uspgredg2vtxeu  29808  wlkon2n0  30252  spthonepeq  30345  usgr2wlkneq  30349  2pthon3v  30539  umgr2adedgspth  30544  clwwlknondisj  30709  frgr2wwlkeqm  30939  2wspmdisj  30945  ajmoi  31467  chocunii  31910  3oalem2  32272  adjmo  32441  cdjreui  33041  eqtrb  33119  probun  35099  bnj551  35421  fineqvnttrclselem1  35847  satfv0fun  36224  satffunlem  36254  satffunlem1lem1  36255  satffunlem2lem1  36257  r1peuqusdeg1  36496  btwnswapid  36876  bj-snsetex  37970  bj-bary1lem1  38339  poimirlem4  38649  exidu1  38897  rngoideu  38944  disjimrmoeqec  39847  mapdpglem31  42867  grpods  43351  remul01  43565  frege55b  45004  frege55c  45025  cncfiooicclem1  47010  euoreqb  48286  isuspgrim0lem  49098  aacllem  51121