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

Theorem eqtr 2313
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 2302 . 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 1632
This theorem is referenced by:  eqtr2  2314  eqtr3  2315  sylan9eq  2348  eqvinc  2908  uneqdifeq  3555  preqsn  3808  relresfld  5215  relcoi1  5217  unixpid  5223  eqer  6709  xpider  6746  undifixp  6868  wemaplem2  7278  infeq5  7354  ficard  8203  winalim2  8334  uzindOLD  10122  pospo  14123  istos  14157  rngodm1dm2  21101  rngoidmlem  21106  rngo1cl  21112  rngoueqz  21113  eqvincg  23146  poseq  24324  soseq  24325  ordcmp  24958  itg2addnclem2  25004  neiopne  25154  oooeqim2  25156  domfldref  25164  rnintintrn  25229  sssu  25244  injsurinj  25252  cbcpcp  25265  jidd  25295  midd  25296  valcurfn1  25307  preoref22  25332  defse3  25375  dfps2  25392  isdir2  25395  ridlideq  25438  rzrlzreq  25439  grpodivone  25476  rngmgmbs3  25520  rngodmeqrn  25522  zerdivemp1  25539  svs2  25590  islimrs4  25685  bwt2  25695  cnegvex2  25763  rnegvex2  25764  addcanrg  25770  negveud  25771  negveudr  25772  hdrmp  25809  imonclem  25916  isepic  25927  prismorcsetlemc  26020  grphidmor2  26056  cmpmor  26078  pgapspf2  26156  isibcg  26294  zerdivemp1x  26689  bnj545  29243  bnj934  29283  bnj953  29287  dvheveccl  31924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator