Theorem eqtr2 2756

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  eqvincg  3636  reusv3i  5402  moop2  5502  relopabi  5822  relop  5850  f0rn0  6776  fliftfun  7311  soseq  8147  addlsub  11634  wrd2ind  14677  fsum2dlem  15720  fprodser  15897  0dvds  16224  cncongr1  16608  4sqlem12  16893  cshwshashlem1  17033  catideu  17623  pj1eu  19605  lspsneu  20881  1marepvmarrepid  22297  mdetunilem6  22339  qtopeu  23440  qtophmeo  23541  dscmet  24301  isosctrlem2  26548  ppiub  26931  sltsolem1  27402  nolt02o  27422  nogt01o  27423  axcgrtr  28428  axeuclid  28476  axcontlem2  28478  uhgr2edg  28720  usgredgreu  28730  uspgredg2vtxeu  28732  wlkon2n0  29178  spthonepeq  29264  usgr2wlkneq  29268  2pthon3v  29452  umgr2adedgspth  29457  clwwlknondisj  29619  frgr2wwlkeqm  29839  2wspmdisj  29845  ajmoi  30366  chocunii  30809  3oalem2  31171  adjmo  31340  cdjreui  31940  eqtrb  31969  probun  33704  bnj551  34039  satfv0fun  34648  satffunlem  34678  satffunlem1lem1  34679  satffunlem2lem1  34681  btwnswapid  35281  bj-snsetex  36147  bj-bary1lem1  36495  poimirlem4  36795  exidu1  37027  rngoideu  37074  mapdpglem31  40877  remul01  41582  frege55b  42950  frege55c  42971  cncfiooicclem1  44908  euoreqb  46116  aacllem  47936