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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqvincg  3605  reusv3i  5346  moop2  5449  relopabi  5769  relop  5797  f0rn0  6713  fliftfun  7253  soseq  8099  addlsub  11555  wrd2ind  14648  fsum2dlem  15696  fprodser  15875  0dvds  16206  cncongr1  16597  4sqlem12  16887  cshwshashlem1  17026  catideu  17600  pj1eu  19594  lspsneu  21049  1marepvmarrepid  22479  mdetunilem6  22521  qtopeu  23620  qtophmeo  23721  dscmet  24477  isosctrlem2  26746  ppiub  27132  sltsolem1  27604  nolt02o  27624  nogt01o  27625  axcgrtr  28879  axeuclid  28927  axcontlem2  28929  uhgr2edg  29172  usgredgreu  29182  uspgredg2vtxeu  29184  wlkon2n0  29629  spthonepeq  29716  usgr2wlkneq  29720  2pthon3v  29907  umgr2adedgspth  29912  clwwlknondisj  30074  frgr2wwlkeqm  30294  2wspmdisj  30300  ajmoi  30821  chocunii  31264  3oalem2  31626  adjmo  31795  cdjreui  32395  eqtrb  32437  probun  34406  bnj551  34728  satfv0fun  35363  satffunlem  35393  satffunlem1lem1  35394  satffunlem2lem1  35396  r1peuqusdeg1  35635  btwnswapid  36010  bj-snsetex  36956  bj-bary1lem1  37304  poimirlem4  37623  exidu1  37855  rngoideu  37902  mapdpglem31  41702  grpods  42187  remul01  42400  frege55b  43890  frege55c  43911  cncfiooicclem1  45894  euoreqb  47113  isuspgrim0lem  47897  aacllem  49806