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

Theorem eqtr3 2472
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 2458 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2470 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 478 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-cleq 2444
This theorem is referenced by:  neneor  2722  eueq  3210  euind  3225  reuind  3243  prnebg  4157  preqsn  4159  eusv1  4597  restidsing  5161  xpcan  5273  xpcan2  5274  funopg  5614  foco  5803  mpt2fun  6398  wfr3g  7034  oawordeulem  7255  ixpfi2  7872  wemapso2lem  8067  isf32lem2  8784  fpwwe2lem13  9067  1re  9642  receu  10257  xrlttri  11438  injresinjlem  12024  cshwsexa  12923  fsumparts  13866  odd2np1  14365  prmreclem2  14861  divsfval  15453  isprs  16175  psrn  16455  grpinveu  16700  symgextf1  17062  symgfixf1  17078  efgrelexlemb  17400  lspextmo  18279  evlseu  18739  tgcmp  20416  sqf11  24066  dchrisumlem2  24328  axlowdimlem15  24986  axcontlem2  24995  nbgraf1olem1  25169  spthonepeq  25317  usgrcyclnl2  25369  4cycl4dv  25395  wwlkextinj  25458  numclwlk1lem2f1  25822  grpoinveu  25950  5oalem4  27310  rnbra  27760  xreceu  28391  bnj594  29723  bnj953  29750  frr3g  30513  sltsolem1  30557  nocvxminlem  30579  fnsingle  30686  funimage  30695  funtransport  30798  funray  30907  funline  30909  hilbert1.2  30922  lineintmo  30924  bj-bary1  31717  poimirlem13  31953  poimirlem14  31954  poimirlem17  31957  poimirlem27  31967  prtlem11  32438  prter2  32453  cdleme  34127  kelac2lem  35922  frege124d  36353  ssprsseq  39002  funsndifnop  39022  2ffzoeq  39064
  Copyright terms: Public domain W3C validator