Theorem eqtr2 2784

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  eqvincg  3605  reusv3i  5373  moop2  5481  relopabiOLD  5810  relop  5838  f0rn0  6797  fliftfun  7351  soseq  8213  addlsub  11771  wrd2ind  14914  fsum2dlem  15980  fprodser  16160  0dvds  16490  cncongr1  16886  4sqlem12  17178  cshwshashlem1  17317  catideu  17899  pj1eu  19961  lspsneu  21452  1marepvmarrepid  22945  mdetunilem6  22987  qtopeu  24090  qtophmeo  24191  dscmet  24946  isosctrlem2  27204  ppiub  27588  ltssolem1  28089  nolt02o  28109  nogt01o  28110  axcgrtr  29550  axeuclid  29598  axcontlem2  29600  uhgr2edg  29846  usgredgreu  29856  uspgredg2vtxeu  29858  wlkon2n0  30302  spthonepeq  30395  usgr2wlkneq  30399  2pthon3v  30589  umgr2adedgspth  30594  clwwlknondisj  30759  frgr2wwlkeqm  30989  2wspmdisj  30995  ajmoi  31517  chocunii  31960  3oalem2  32322  adjmo  32491  cdjreui  33091  eqtrb  33169  probun  35162  bnj551  35484  fineqvnttrclselem1  35930  satfv0fun  36344  satffunlem  36374  satffunlem1lem1  36375  satffunlem2lem1  36377  r1peuqusdeg1  36616  btwnswapid  36997  bj-snsetex  38091  bj-bary1lem1  38500  poimirlem4  38810  exidu1  39056  rngoideu  39103  disjimrmoeqec  40006  mapdpglem31  43026  grpods  43510  remul01  43724  frege55b  45158  frege55c  45179  cncfiooicclem1  47176  euoreqb  48453  isuspgrim0lem  49264  aacllem  51367