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

Theorem eqtr 2301
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 2290 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21biimpar 473 1  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1628
This theorem is referenced by:  eqtr2  2302  eqtr3  2303  sylan9eq  2336  eqvinc  2896  uneqdifeq  3543  preqsn  3793  relresfld  5197  relcoi1  5199  unixpid  5205  eqer  6688  xpider  6725  undifixp  6847  wemaplem2  7257  infeq5  7333  ficard  8182  winalim2  8313  uzindOLD  10101  pospo  14101  istos  14135  rngodm1dm2  21077  rngoidmlem  21082  rngo1cl  21088  rngoueqz  21089  poseq  23654  soseq  23655  elfuns  23861  ordcmp  24293  neiopne  24449  oooeqim2  24451  domfldref  24459  rnintintrn  24525  sssu  24540  injsurinj  24548  repfuntw  24559  cbcpcp  24561  jidd  24591  midd  24592  valcurfn1  24603  preoref22  24628  defse3  24671  dfps2  24688  isdir2  24691  ridlideq  24734  rzrlzreq  24735  grpodivone  24772  rngmgmbs3  24816  rngodmeqrn  24818  zerdivemp1  24835  svs2  24886  islimrs4  24981  bwt2  24991  cnegvex2  25059  rnegvex2  25060  addcanrg  25066  negveud  25067  negveudr  25068  hdrmp  25105  imonclem  25212  isepic  25223  prismorcsetlemc  25316  grphidmor2  25352  cmpmor  25374  pgapspf2  25452  isibcg  25590  zerdivemp1x  25985  bnj545  28194  bnj934  28234  bnj953  28238  dvheveccl  30569
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-11 1719  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-cleq 2277
  Copyright terms: Public domain W3C validator