MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 eqeq1 2737 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21biimpa 478 1 ((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  eqvincg  3599  reusv3i  5360  moop2  5460  relopabi  5779  relop  5807  f0rn0  6728  fliftfun  7258  soseq  8092  addlsub  11576  wrd2ind  14617  fsum2dlem  15660  fprodser  15837  0dvds  16164  cncongr1  16548  4sqlem12  16833  cshwshashlem1  16973  catideu  17560  pj1eu  19483  lspsneu  20600  1marepvmarrepid  21940  mdetunilem6  21982  qtopeu  23083  qtophmeo  23184  dscmet  23944  isosctrlem2  26185  ppiub  26568  sltsolem1  27039  nolt02o  27059  nogt01o  27060  axcgrtr  27906  axeuclid  27954  axcontlem2  27956  uhgr2edg  28198  usgredgreu  28208  uspgredg2vtxeu  28210  wlkon2n0  28656  spthonepeq  28742  usgr2wlkneq  28746  2pthon3v  28930  umgr2adedgspth  28935  clwwlknondisj  29097  frgr2wwlkeqm  29317  2wspmdisj  29323  ajmoi  29842  chocunii  30285  3oalem2  30647  adjmo  30816  cdjreui  31416  eqtrb  31445  probun  33076  bnj551  33411  satfv0fun  34022  satffunlem  34052  satffunlem1lem1  34053  satffunlem2lem1  34055  btwnswapid  34648  bj-snsetex  35480  bj-bary1lem1  35828  poimirlem4  36128  exidu1  36361  rngoideu  36408  mapdpglem31  40212  remul01  40919  frege55b  42257  frege55c  42278  cncfiooicclem1  44220  euoreqb  45427  aacllem  47334
  Copyright terms: Public domain W3C validator