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 480	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  eqvincg  3606  reusv3i  5358  moop2  5468  relopabi  5791  relop  5818  f0rn0  6744  fliftfun  7291  soseq  8133  addlsub  11597  wrd2ind  14730  fsum2dlem  15788  fprodser  15970  0dvds  16301  cncongr1  16692  4sqlem12  16983  cshwshashlem1  17122  catideu  17698  pj1eu  19727  lspsneu  21181  1marepvmarrepid  22623  mdetunilem6  22665  qtopeu  23764  qtophmeo  23865  dscmet  24620  isosctrlem2  26872  ppiub  27256  ltssolem1  27727  nolt02o  27747  nogt01o  27748  axcgrtr  29073  axeuclid  29121  axcontlem2  29123  uhgr2edg  29366  usgredgreu  29376  uspgredg2vtxeu  29378  wlkon2n0  29822  spthonepeq  29909  usgr2wlkneq  29913  2pthon3v  30100  umgr2adedgspth  30105  clwwlknondisj  30270  frgr2wwlkeqm  30490  2wspmdisj  30496  ajmoi  31018  chocunii  31461  3oalem2  31823  adjmo  31992  cdjreui  32592  eqtrb  32632  probun  34677  bnj551  34999  fineqvnttrclselem1  35378  satfv0fun  35682  satffunlem  35712  satffunlem1lem1  35713  satffunlem2lem1  35715  r1peuqusdeg1  35954  btwnswapid  36328  bj-snsetex  37409  bj-bary1lem1  37764  poimirlem4  38084  exidu1  38316  rngoideu  38363  disjimrmoeqec  39268  mapdpglem31  42288  grpods  42772  remul01  42977  frege55b  44434  frege55c  44455  cncfiooicclem1  46428  euoreqb  47664  isuspgrim0lem  48476  aacllem  50383