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

Theorem eqtr3 2315
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 2298 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2313 . 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 1632
This theorem is referenced by:  eueq  2950  euind  2965  reuind  2981  preqsn  3808  eusv1  4544  xpcan  5128  xpcan2  5129  funopg  5302  foco  5477  mpt2fun  5962  oawordeulem  6568  ixpfi2  7170  wemapso2  7283  isf32lem2  7996  fpwwe2lem13  8280  1re  8853  receu  9429  xrlttri  10489  fsumparts  12280  odd2np1  12603  prmreclem2  12980  divsfval  13465  isprs  14080  psrn  14334  grpinveu  14532  efgrelexlemb  15075  lspextmo  15829  tgcmp  17144  evlseu  19416  sqf11  20393  dchrisumlema  20653  dchrisumlem2  20655  grpoinveu  20905  5oalem4  22252  rnbra  22703  xreceu  23121  wfr3g  24326  frr3g  24351  sltsolem1  24393  nocvxminlem  24415  fnsingle  24529  funimage  24538  axlowdimlem15  24656  axcontlem2  24665  funtransport  24726  funray  24835  funline  24837  hilbert1.2  24850  lineintmo  24852  restidsing  25179  imonclem  25916  ismonc  25917  prtlem11  26837  prter2  26852  kelac2lem  27265  injresinjlem  28214  usgrcyclnl2  28387  4cycl4dv  28413  bnj594  29260  bnj953  29287  cdleme  31371
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator