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

Theorem eqtr2 2822
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Assertion
Ref Expression
eqtr2 ((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)

Proof of Theorem eqtr2
StepHypRef Expression
1 eqcom 2808 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
2 eqtr 2821 . 2 ((𝐵 = 𝐴𝐴 = 𝐶) → 𝐵 = 𝐶)
31, 2sylanb 584 1 ((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538
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 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794
This theorem is referenced by:  eqvincg  3592  reusv3i  5273  moop2  5360  relopabi  5662  relop  5689  f0rn0  6542  fliftfun  7048  addlsub  11049  wrd2ind  14080  fsum2dlem  15120  fprodser  15298  0dvds  15625  cncongr1  16004  4sqlem12  16285  cshwshashlem1  16424  catideu  16941  pj1eu  18817  lspsneu  19891  1marepvmarrepid  21183  mdetunilem6  21225  qtopeu  22324  qtophmeo  22425  dscmet  23182  isosctrlem2  25408  ppiub  25791  axcgrtr  26712  axeuclid  26760  axcontlem2  26762  uhgr2edg  27001  usgredgreu  27011  uspgredg2vtxeu  27013  wlkon2n0  27459  spthonepeq  27544  usgr2wlkneq  27548  2pthon3v  27732  umgr2adedgspth  27737  clwwlknondisj  27899  frgr2wwlkeqm  28119  2wspmdisj  28125  ajmoi  28644  chocunii  29087  3oalem2  29449  adjmo  29618  cdjreui  30218  eqtrb  30248  probun  31785  bnj551  32121  satfv0fun  32726  satffunlem  32756  satffunlem1lem1  32757  satffunlem2lem1  32759  soseq  33204  sltsolem1  33288  nolt02o  33307  btwnswapid  33586  bj-snsetex  34394  bj-bary1lem1  34720  poimirlem4  35054  exidu1  35287  rngoideu  35334  mapdpglem31  38992  remul01  39532  frege55b  40585  frege55c  40606  cncfiooicclem1  42522  euoreqb  43652  aacllem  45316
  Copyright terms: Public domain W3C validator