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

Theorem eqtr2 2461
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 2445 . 2  |-  ( A  =  B  <->  B  =  A )
2 eqtr 2460 . 2  |-  ( ( B  =  A  /\  A  =  C )  ->  B  =  C )
31, 2sylanb 460 1  |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1654
This theorem is referenced by:  eqvinc  3072  moop2  4486  reusv3i  4765  relop  5058  fliftfun  6070  th3qlem1  7046  fsum2dlem  12592  0dvds  12908  4sqlem12  13362  catideu  13938  pj1eu  15366  lspsneu  16233  bwth  17511  qtopeu  17786  qtophmeo  17887  dscmet  18658  isosctrlem2  20701  ppiub  21026  usgraedgprv  21434  usgra2edg  21440  usgraedgreu  21445  spthonepeq  21625  wlkdvspthlem  21645  exidu1  21952  rngoideu  22010  ajmoi  22398  chocunii  22841  3oalem2  23203  adjmo  23373  cdjreui  23973  eqvincg  23999  probun  24712  fprodser  25310  soseq  25564  sltsolem1  25658  axcgrtr  25889  axeuclid  25937  axcontlem2  25939  btwnswapid  25986  f0rn0  28191  usgra2wlkspthlem1  28442  el2wlkonotot0  28502  2spotdisj  28622  bnj551  29284  mapdpglem31  32675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-11 1764  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2436
  Copyright terms: Public domain W3C validator