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

Theorem eqtr2 2301
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 2285 . 2  |-  ( A  =  B  <->  B  =  A )
2 eqtr 2300 . 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 1623
This theorem is referenced by:  eqvinc  2895  moop2  4261  reusv3i  4541  relop  4834  fliftfun  5811  th3qlem1  6764  fsum2dlem  12233  0dvds  12549  4sqlem12  13003  catideu  13577  pj1eu  15005  lspsneu  15876  qtopeu  17407  qtophmeo  17508  dscmet  18095  isosctrlem2  20119  ppiub  20443  exidu1  20993  rngoideu  21051  ajmoi  21437  chocunii  21880  3oalem2  22242  adjmo  22412  cdjreui  23012  eqvincg  23130  soseq  24254  sltsolem1  24322  axcgrtr  24543  axeuclid  24591  axcontlem2  24593  btwnswapid  24640  restidsing  25076  bwt2  25592  bsstrs  26146  usgraedgprv  28122  bnj551  28771  mapdpglem31  31893
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator