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 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 2732

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

This theorem is used by:  eqvincg  3602  reusv3i  5369  moop2  5479  relopabi  5803  relop  5830  f0rn0  6760  fliftfun  7313  soseq  8157  addlsub  11654  wrd2ind  14792  fsum2dlem  15856  fprodser  16036  0dvds  16366  cncongr1  16757  4sqlem12  17048  cshwshashlem1  17187  catideu  17763  pj1eu  19823  lspsneu  21310  1marepvmarrepid  22797  mdetunilem6  22839  qtopeu  23942  qtophmeo  24043  dscmet  24798  isosctrlem2  27056  ppiub  27440  ltssolem1  27911  nolt02o  27931  nogt01o  27932  axcgrtr  29372  axeuclid  29420  axcontlem2  29422  uhgr2edg  29668  usgredgreu  29678  uspgredg2vtxeu  29680  wlkon2n0  30124  spthonepeq  30217  usgr2wlkneq  30221  2pthon3v  30411  umgr2adedgspth  30416  clwwlknondisj  30581  frgr2wwlkeqm  30811  2wspmdisj  30817  ajmoi  31339  chocunii  31782  3oalem2  32144  adjmo  32313  cdjreui  32913  eqtrb  32949  probun  34930  bnj551  35252  fineqvnttrclselem1  35647  satfv0fun  35950  satffunlem  35980  satffunlem1lem1  35981  satffunlem2lem1  35983  r1peuqusdeg1  36222  btwnswapid  36597  bj-snsetex  37707  bj-bary1lem1  38063  poimirlem4  38373  exidu1  38606  rngoideu  38653  disjimrmoeqec  39556  mapdpglem31  42576  grpods  43060  remul01  43282  frege55b  44737  frege55c  44758  cncfiooicclem1  46721  euoreqb  47997  isuspgrim0lem  48809  aacllem  50772