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  3611  reusv3i  5354  moop2  5457  relopabi  5776  relop  5804  f0rn0  6727  fliftfun  7269  soseq  8115  addlsub  11570  wrd2ind  14664  fsum2dlem  15712  fprodser  15891  0dvds  16222  cncongr1  16613  4sqlem12  16903  cshwshashlem1  17042  catideu  17612  pj1eu  19602  lspsneu  21009  1marepvmarrepid  22438  mdetunilem6  22480  qtopeu  23579  qtophmeo  23680  dscmet  24436  isosctrlem2  26705  ppiub  27091  sltsolem1  27563  nolt02o  27583  nogt01o  27584  axcgrtr  28818  axeuclid  28866  axcontlem2  28868  uhgr2edg  29111  usgredgreu  29121  uspgredg2vtxeu  29123  wlkon2n0  29568  spthonepeq  29655  usgr2wlkneq  29659  2pthon3v  29846  umgr2adedgspth  29851  clwwlknondisj  30013  frgr2wwlkeqm  30233  2wspmdisj  30239  ajmoi  30760  chocunii  31203  3oalem2  31565  adjmo  31734  cdjreui  32334  eqtrb  32376  probun  34383  bnj551  34705  satfv0fun  35331  satffunlem  35361  satffunlem1lem1  35362  satffunlem2lem1  35364  r1peuqusdeg1  35603  btwnswapid  35978  bj-snsetex  36924  bj-bary1lem1  37272  poimirlem4  37591  exidu1  37823  rngoideu  37870  mapdpglem31  41670  grpods  42155  remul01  42368  frege55b  43859  frege55c  43880  cncfiooicclem1  45864  euoreqb  47083  isuspgrim0lem  47866  aacllem  49763