Theorem eqtr2 2751

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719

This theorem is referenced by:  eqvincg  3632  reusv3i  5398  moop2  5498  relopabi  5818  relop  5847  f0rn0  6776  fliftfun  7314  soseq  8158  addlsub  11652  wrd2ind  14697  fsum2dlem  15740  fprodser  15917  0dvds  16245  cncongr1  16629  4sqlem12  16916  cshwshashlem1  17056  catideu  17646  pj1eu  19642  lspsneu  21000  1marepvmarrepid  22464  mdetunilem6  22506  qtopeu  23607  qtophmeo  23708  dscmet  24468  isosctrlem2  26738  ppiub  27124  sltsolem1  27595  nolt02o  27615  nogt01o  27616  axcgrtr  28713  axeuclid  28761  axcontlem2  28763  uhgr2edg  29008  usgredgreu  29018  uspgredg2vtxeu  29020  wlkon2n0  29467  spthonepeq  29553  usgr2wlkneq  29557  2pthon3v  29741  umgr2adedgspth  29746  clwwlknondisj  29908  frgr2wwlkeqm  30128  2wspmdisj  30134  ajmoi  30655  chocunii  31098  3oalem2  31460  adjmo  31629  cdjreui  32229  eqtrb  32258  probun  33975  bnj551  34309  satfv0fun  34917  satffunlem  34947  satffunlem1lem1  34948  satffunlem2lem1  34950  btwnswapid  35549  bj-snsetex  36378  bj-bary1lem1  36726  poimirlem4  37032  exidu1  37264  rngoideu  37311  mapdpglem31  41113  remul01  41884  frege55b  43250  frege55c  43271  cncfiooicclem1  45204  euoreqb  46412  isuspgrim0lem  47092  aacllem  48157