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

Theorem eqtr2 2314
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 2298 . 2  |-  ( A  =  B  <->  B  =  A )
2 eqtr 2313 . 2  |-  ( ( B  =  A  /\  A  =  C )  ->  B  =  C )
31, 2sylanb 458 1  |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632
This theorem is referenced by:  eqvinc  2908  moop2  4277  reusv3i  4557  relop  4850  fliftfun  5827  th3qlem1  6780  fsum2dlem  12249  0dvds  12565  4sqlem12  13019  catideu  13593  pj1eu  15021  lspsneu  15892  qtopeu  17423  qtophmeo  17524  dscmet  18111  isosctrlem2  20135  ppiub  20459  exidu1  21009  rngoideu  21067  ajmoi  21453  chocunii  21896  3oalem2  22258  adjmo  22428  cdjreui  23028  eqvincg  23146  soseq  24325  sltsolem1  24393  axcgrtr  24615  axeuclid  24663  axcontlem2  24665  btwnswapid  24712  restidsing  25179  bwt2  25695  bsstrs  26249  usgraedgprv  28256  wlkdvspthlem  28365  bnj551  29087  mapdpglem31  32515
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator