Theorem eqtr2 2757

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  eqvincg  3590  reusv3i  5346  moop2  5456  relopabi  5778  relop  5805  f0rn0  6725  fliftfun  7267  soseq  8109  addlsub  11566  wrd2ind  14685  fsum2dlem  15732  fprodser  15914  0dvds  16245  cncongr1  16636  4sqlem12  16927  cshwshashlem1  17066  catideu  17641  pj1eu  19671  lspsneu  21121  1marepvmarrepid  22540  mdetunilem6  22582  qtopeu  23681  qtophmeo  23782  dscmet  24537  isosctrlem2  26783  ppiub  27167  ltssolem1  27639  nolt02o  27659  nogt01o  27660  axcgrtr  28984  axeuclid  29032  axcontlem2  29034  uhgr2edg  29277  usgredgreu  29287  uspgredg2vtxeu  29289  wlkon2n0  29733  spthonepeq  29820  usgr2wlkneq  29824  2pthon3v  30011  umgr2adedgspth  30016  clwwlknondisj  30181  frgr2wwlkeqm  30401  2wspmdisj  30407  ajmoi  30929  chocunii  31372  3oalem2  31734  adjmo  31903  cdjreui  32503  eqtrb  32543  probun  34563  bnj551  34885  fineqvnttrclselem1  35265  satfv0fun  35553  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  r1peuqusdeg1  35825  btwnswapid  36199  bj-snsetex  37270  bj-bary1lem1  37625  poimirlem4  37945  exidu1  38177  rngoideu  38224  disjimrmoeqec  39129  mapdpglem31  42149  grpods  42633  remul01  42839  frege55b  44324  frege55c  44345  cncfiooicclem1  46321  euoreqb  47557  isuspgrim0lem  48369  aacllem  50276