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

Theorem eqtr3 2302
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 2285 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2300 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 461 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623
This theorem is referenced by:  eueq  2937  euind  2952  reuind  2968  preqsn  3792  eusv1  4528  xpcan  5112  xpcan2  5113  funopg  5286  foco  5461  mpt2fun  5946  oawordeulem  6552  ixpfi2  7154  wemapso2  7267  isf32lem2  7980  fpwwe2lem13  8264  1re  8837  receu  9413  xrlttri  10473  fsumparts  12264  odd2np1  12587  prmreclem2  12964  divsfval  13449  isprs  14064  psrn  14318  grpinveu  14516  efgrelexlemb  15059  lspextmo  15813  tgcmp  17128  evlseu  19400  sqf11  20377  dchrisumlema  20637  dchrisumlem2  20639  grpoinveu  20889  5oalem4  22236  rnbra  22687  wfr3g  23666  frr3g  23691  sltsolem1  23733  nocvxminlem  23755  fnsingle  23869  funimage  23878  axlowdimlem15  23995  axcontlem2  24004  funtransport  24065  funray  24174  funline  24176  hilbert1.2  24189  lineintmo  24191  restidsing  24488  imonclem  25225  ismonc  25226  prtlem11  26146  prter2  26161  kelac2lem  26574  bnj594  28317  bnj953  28344  cdleme  30122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator