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

Theorem eqtr 2300
Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
Assertion
Ref Expression
eqtr  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )

Proof of Theorem eqtr
StepHypRef Expression
1 eqeq1 2289 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21biimpar 471 1  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623
This theorem is referenced by:  eqtr2  2301  eqtr3  2302  sylan9eq  2335  eqvinc  2895  uneqdifeq  3542  preqsn  3792  relresfld  5199  relcoi1  5201  unixpid  5207  eqer  6693  xpider  6730  undifixp  6852  wemaplem2  7262  infeq5  7338  ficard  8187  winalim2  8318  uzindOLD  10106  pospo  14107  istos  14141  rngodm1dm2  21085  rngoidmlem  21090  rngo1cl  21096  rngoueqz  21097  eqvincg  23130  poseq  24253  soseq  24254  ordcmp  24886  neiopne  25051  oooeqim2  25053  domfldref  25061  rnintintrn  25126  sssu  25141  injsurinj  25149  cbcpcp  25162  jidd  25192  midd  25193  valcurfn1  25204  preoref22  25229  defse3  25272  dfps2  25289  isdir2  25292  ridlideq  25335  rzrlzreq  25336  grpodivone  25373  rngmgmbs3  25417  rngodmeqrn  25419  zerdivemp1  25436  svs2  25487  islimrs4  25582  bwt2  25592  cnegvex2  25660  rnegvex2  25661  addcanrg  25667  negveud  25668  negveudr  25669  hdrmp  25706  imonclem  25813  isepic  25824  prismorcsetlemc  25917  grphidmor2  25953  cmpmor  25975  pgapspf2  26053  isibcg  26191  zerdivemp1x  26586  bnj545  28927  bnj934  28967  bnj953  28971  dvheveccl  31302
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