Theorem eqtr2 2782

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 2765	. 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 2155  ax-ext 2733

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

This theorem is used by:  eqvincg  3602  reusv3i  5366  moop2  5474  relopabi  5800  relop  5828  f0rn0  6765  fliftfun  7318  soseq  8169  addlsub  11725  wrd2ind  14865  fsum2dlem  15929  fprodser  16109  0dvds  16439  cncongr1  16835  4sqlem12  17127  cshwshashlem1  17266  catideu  17842  pj1eu  19903  lspsneu  21394  1marepvmarrepid  22883  mdetunilem6  22925  qtopeu  24028  qtophmeo  24129  dscmet  24884  isosctrlem2  27140  ppiub  27524  ltssolem1  28025  nolt02o  28045  nogt01o  28046  axcgrtr  29486  axeuclid  29534  axcontlem2  29536  uhgr2edg  29782  usgredgreu  29792  uspgredg2vtxeu  29794  wlkon2n0  30238  spthonepeq  30331  usgr2wlkneq  30335  2pthon3v  30525  umgr2adedgspth  30530  clwwlknondisj  30695  frgr2wwlkeqm  30925  2wspmdisj  30931  ajmoi  31453  chocunii  31896  3oalem2  32258  adjmo  32427  cdjreui  33027  eqtrb  33063  probun  35044  bnj551  35366  fineqvnttrclselem1  35772  satfv0fun  36115  satffunlem  36145  satffunlem1lem1  36146  satffunlem2lem1  36148  r1peuqusdeg1  36387  btwnswapid  36762  bj-snsetex  37856  bj-bary1lem1  38212  poimirlem4  38522  exidu1  38770  rngoideu  38817  disjimrmoeqec  39720  mapdpglem31  42740  grpods  43224  remul01  43438  frege55b  44882  frege55c  44903  cncfiooicclem1  46872  euoreqb  48148  isuspgrim0lem  48960  aacllem  50908