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

Theorem eqtr3 2456
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 2439 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2454 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 463 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653
This theorem is referenced by:  eueq  3107  euind  3122  reuind  3138  prnebg  3980  preqsn  3981  eusv1  4718  xpcan  5306  xpcan2  5307  funopg  5486  foco  5664  mpt2fun  6173  oawordeulem  6798  ixpfi2  7406  wemapso2  7522  isf32lem2  8235  fpwwe2lem13  8518  1re  9091  receu  9668  xrlttri  10733  injresinjlem  11200  fsumparts  12586  odd2np1  12909  prmreclem2  13286  divsfval  13773  isprs  14388  psrn  14642  grpinveu  14840  efgrelexlemb  15383  lspextmo  16133  tgcmp  17465  evlseu  19938  sqf11  20923  dchrisumlem2  21185  nbgraf1olem1  21452  spthonepeq  21588  usgrcyclnl2  21629  4cycl4dv  21655  grpoinveu  21811  5oalem4  23160  rnbra  23611  xreceu  24169  wfr3g  25538  frr3g  25582  sltsolem1  25624  nocvxminlem  25646  fnsingle  25765  funimage  25774  axlowdimlem15  25896  axcontlem2  25905  funtransport  25966  funray  26075  funline  26077  hilbert1.2  26090  lineintmo  26092  prtlem11  26716  prter2  26731  kelac2lem  27140  2ffzoeq  28141  cshwsexa  28292  bnj594  29284  bnj953  29311  cdleme  31358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2430
  Copyright terms: Public domain W3C validator