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

Theorem eqtr3 2406
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 2389 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2404 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 462 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649
This theorem is referenced by:  eueq  3049  euind  3064  reuind  3080  prnebg  3921  preqsn  3922  eusv1  4657  xpcan  5245  xpcan2  5246  funopg  5425  foco  5603  mpt2fun  6111  oawordeulem  6733  ixpfi2  7340  wemapso2  7454  isf32lem2  8167  fpwwe2lem13  8450  1re  9023  receu  9599  xrlttri  10664  injresinjlem  11126  fsumparts  12512  odd2np1  12835  prmreclem2  13212  divsfval  13699  isprs  14314  psrn  14568  grpinveu  14766  efgrelexlemb  15309  lspextmo  16059  tgcmp  17386  evlseu  19804  sqf11  20789  dchrisumlem2  21051  nbgraf1olem1  21317  usgrcyclnl2  21476  4cycl4dv  21502  grpoinveu  21658  5oalem4  23007  rnbra  23458  xreceu  24006  wfr3g  25279  frr3g  25304  sltsolem1  25346  nocvxminlem  25368  fnsingle  25482  funimage  25491  axlowdimlem15  25609  axcontlem2  25618  funtransport  25679  funray  25788  funline  25790  hilbert1.2  25803  lineintmo  25805  prtlem11  26406  prter2  26421  kelac2lem  26831  bnj594  28621  bnj953  28648  cdleme  30674
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2380
  Copyright terms: Public domain W3C validator