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 475 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2446
This theorem is referenced by:  eueq  3238  euind  3253  reuind  3270  prnebg  4165  preqsn  4166  eusv1  4597  restidsing  5273  xpcan  5385  xpcan2  5386  funopg  5561  foco  5741  mpt2fun  6305  oawordeulem  7106  ixpfi2  7723  wemapso2OLD  7880  wemapso2lem  7881  isf32lem2  8637  fpwwe2lem13  8923  1re  9499  receu  10095  xrlttri  11230  injresinjlem  11758  hash2prd  12302  cshwsexa  12579  fsumparts  13390  odd2np1  13713  prmreclem2  14099  divsfval  14607  isprs  15222  psrn  15501  grpinveu  15694  symgextf1  16048  symgfixf1  16065  efgrelexlemb  16371  lspextmo  17263  evlseu  17729  tgcmp  19139  sqf11  22613  dchrisumlem2  22875  axlowdimlem15  23374  axcontlem2  23383  nbgraf1olem1  23522  spthonepeq  23658  usgrcyclnl2  23699  4cycl4dv  23725  grpoinveu  23881  5oalem4  25232  rnbra  25683  xreceu  26262  wfr3g  27887  frr3g  27931  sltsolem1  27973  nocvxminlem  27995  fnsingle  28114  funimage  28123  funtransport  28226  funray  28335  funline  28337  hilbert1.2  28350  lineintmo  28352  prtlem11  29179  prter2  29194  kelac2lem  29585  2ffzoeq  30382  wwlkextinj  30530  numclwlk1lem2f1  30855  bnj594  32257  bnj953  32284  bj-bary1  32959  cdleme  34562
  Copyright terms: Public domain W3C validator