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

Theorem eqtr3 2471
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 2452 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2469 . 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 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2435
This theorem is referenced by:  eueq  3257  euind  3272  reuind  3289  prnebg  4197  preqsn  4198  eusv1  4631  restidsing  5320  xpcan  5433  xpcan2  5434  funopg  5610  foco  5795  mpt2fun  6389  oawordeulem  7205  ixpfi2  7820  wemapso2OLD  7980  wemapso2lem  7981  isf32lem2  8737  fpwwe2lem13  9023  1re  9598  receu  10200  xrlttri  11354  injresinjlem  11904  hash2prd  12497  cshwsexa  12771  fsumparts  13599  odd2np1  13923  prmreclem2  14312  divsfval  14821  isprs  15433  psrn  15713  grpinveu  15958  symgextf1  16320  symgfixf1  16336  efgrelexlemb  16642  lspextmo  17576  evlseu  18059  tgcmp  19774  sqf11  23285  dchrisumlem2  23547  axlowdimlem15  24131  axcontlem2  24140  nbgraf1olem1  24313  spthonepeq  24461  usgrcyclnl2  24513  4cycl4dv  24539  wwlkextinj  24602  numclwlk1lem2f1  24966  grpoinveu  25096  5oalem4  26447  rnbra  26898  xreceu  27491  wfr3g  29317  frr3g  29361  sltsolem1  29403  nocvxminlem  29425  fnsingle  29544  funimage  29553  funtransport  29656  funray  29765  funline  29767  hilbert1.2  29780  lineintmo  29782  prtlem11  30582  prter2  30597  kelac2lem  30985  2ffzoeq  32179  bnj594  33698  bnj953  33725  bj-bary1  34415  cdleme  36020
  Copyright terms: Public domain W3C validator