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

Theorem eqtr2 2454
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  |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )

Proof of Theorem eqtr2
StepHypRef Expression
1 eqcom 2438 . 2  |-  ( A  =  B  <->  B  =  A )
2 eqtr 2453 . 2  |-  ( ( B  =  A  /\  A  =  C )  ->  B  =  C )
31, 2sylanb 459 1  |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652
This theorem is referenced by:  eqvinc  3063  moop2  4451  reusv3i  4730  relop  5023  fliftfun  6034  th3qlem1  7010  fsum2dlem  12554  0dvds  12870  4sqlem12  13324  catideu  13900  pj1eu  15328  lspsneu  16195  bwth  17473  qtopeu  17748  qtophmeo  17849  dscmet  18620  isosctrlem2  20663  ppiub  20988  usgraedgprv  21396  usgra2edg  21402  usgraedgreu  21407  spthonepeq  21587  wlkdvspthlem  21607  exidu1  21914  rngoideu  21972  ajmoi  22360  chocunii  22803  3oalem2  23165  adjmo  23335  cdjreui  23935  eqvincg  23961  probun  24677  fprodser  25275  soseq  25529  sltsolem1  25623  axcgrtr  25854  axeuclid  25902  axcontlem2  25904  btwnswapid  25951  usgra2wlkspthlem1  28306  el2wlkonotot0  28339  2spotdisj  28450  bnj551  29110  mapdpglem31  32501
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator