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

Theorem eqtr3 2448
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 2429 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2446 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 477 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2412
This theorem is referenced by:  neneor  2753  eueq  3240  euind  3255  reuind  3272  prnebg  4176  preqsn  4177  eusv1  4610  restidsing  5172  xpcan  5284  xpcan2  5285  funopg  5624  foco  5811  mpt2fun  6403  wfr3g  7033  oawordeulem  7254  ixpfi2  7869  wemapso2lem  8058  isf32lem2  8773  fpwwe2lem13  9056  1re  9631  receu  10246  xrlttri  11427  injresinjlem  12010  hash2prd  12616  cshwsexa  12897  fsumparts  13833  odd2np1  14332  prmreclem2  14813  divsfval  15397  isprs  16119  psrn  16399  grpinveu  16644  symgextf1  17006  symgfixf1  17022  efgrelexlemb  17328  lspextmo  18207  evlseu  18667  tgcmp  20340  sqf11  23926  dchrisumlem2  24188  axlowdimlem15  24829  axcontlem2  24838  nbgraf1olem1  25011  spthonepeq  25159  usgrcyclnl2  25211  4cycl4dv  25237  wwlkextinj  25300  numclwlk1lem2f1  25664  grpoinveu  25792  5oalem4  27142  rnbra  27592  xreceu  28226  bnj594  29508  bnj953  29535  frr3g  30297  sltsolem1  30339  nocvxminlem  30361  fnsingle  30468  funimage  30477  funtransport  30580  funray  30689  funline  30691  hilbert1.2  30704  lineintmo  30706  bj-bary1  31459  poimirlem13  31657  poimirlem14  31658  poimirlem17  31661  poimirlem27  31671  prtlem11  32146  prter2  32161  cdleme  33836  kelac2lem  35632  frege124d  35996  2ffzoeq  38426
  Copyright terms: Public domain W3C validator