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

Theorem eqtr3 2482
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.)
Assertion
Ref Expression
eqtr3  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )

Proof of Theorem eqtr3
StepHypRef Expression
1 eqcom 2463 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2480 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 473 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2446
This theorem is referenced by:  eueq  3268  euind  3283  reuind  3300  prnebg  4198  preqsn  4199  eusv1  4631  restidsing  5318  xpcan  5428  xpcan2  5429  funopg  5602  foco  5787  mpt2fun  6377  oawordeulem  7195  ixpfi2  7810  wemapso2OLD  7969  wemapso2lem  7970  isf32lem2  8725  fpwwe2lem13  9009  1re  9584  receu  10190  xrlttri  11348  injresinjlem  11906  hash2prd  12502  cshwsexa  12783  fsumparts  13702  odd2np1  14130  prmreclem2  14519  divsfval  15036  isprs  15758  psrn  16038  grpinveu  16283  symgextf1  16645  symgfixf1  16661  efgrelexlemb  16967  lspextmo  17897  evlseu  18380  tgcmp  20068  sqf11  23611  dchrisumlem2  23873  axlowdimlem15  24461  axcontlem2  24470  nbgraf1olem1  24643  spthonepeq  24791  usgrcyclnl2  24843  4cycl4dv  24869  wwlkextinj  24932  numclwlk1lem2f1  25296  grpoinveu  25422  5oalem4  26773  rnbra  27224  xreceu  27852  wfr3g  29582  frr3g  29626  sltsolem1  29668  nocvxminlem  29690  fnsingle  29797  funimage  29806  funtransport  29909  funray  30018  funline  30020  hilbert1.2  30033  lineintmo  30035  prtlem11  30847  prter2  30862  kelac2lem  31249  2ffzoeq  32715  bnj594  34371  bnj953  34398  bj-bary1  35078  cdleme  36683
  Copyright terms: Public domain W3C validator