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

Theorem eqtr3 2495
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 2476 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2493 . 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 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459
This theorem is referenced by:  eueq  3275  euind  3290  reuind  3307  prnebg  4208  preqsn  4209  eusv1  4641  restidsing  5329  xpcan  5442  xpcan2  5443  funopg  5619  foco  5804  mpt2fun  6387  oawordeulem  7203  ixpfi2  7817  wemapso2OLD  7976  wemapso2lem  7977  isf32lem2  8733  fpwwe2lem13  9019  1re  9594  receu  10193  xrlttri  11344  injresinjlem  11892  hash2prd  12483  cshwsexa  12754  fsumparts  13582  odd2np1  13904  prmreclem2  14293  divsfval  14801  isprs  15416  psrn  15695  grpinveu  15891  symgextf1  16248  symgfixf1  16265  efgrelexlemb  16571  lspextmo  17497  evlseu  17972  tgcmp  19683  sqf11  23157  dchrisumlem2  23419  axlowdimlem15  23951  axcontlem2  23960  nbgraf1olem1  24133  spthonepeq  24281  usgrcyclnl2  24333  4cycl4dv  24359  wwlkextinj  24422  numclwlk1lem2f1  24787  grpoinveu  24916  5oalem4  26267  rnbra  26718  xreceu  27302  wfr3g  28935  frr3g  28979  sltsolem1  29021  nocvxminlem  29043  fnsingle  29162  funimage  29171  funtransport  29274  funray  29383  funline  29385  hilbert1.2  29398  lineintmo  29400  prtlem11  30227  prter2  30242  kelac2lem  30630  2ffzoeq  31824  bnj594  33058  bnj953  33085  bj-bary1  33762  cdleme  35365
  Copyright terms: Public domain W3C validator