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

Theorem eqtr 2273
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 2262 . 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 1619
This theorem is referenced by:  eqtr2  2274  eqtr3  2275  sylan9eq  2308  eqvinc  2846  uneqdifeq  3484  preqsn  3733  relresfld  5151  relcoi1  5153  unixpid  5159  eqer  6626  xpider  6663  undifixp  6785  wemaplem2  7195  infeq5  7271  ficard  8120  winalim2  8251  uzindOLD  10038  pospo  14034  istos  14068  rngodm1dm2  21010  rngoidmlem  21015  rngo1cl  21021  rngoueqz  21022  poseq  23587  soseq  23588  elfuns  23794  ordcmp  24226  neiopne  24382  oooeqim2  24384  domfldref  24392  rnintintrn  24458  sssu  24473  injsurinj  24481  repfuntw  24492  cbcpcp  24494  jidd  24524  midd  24525  valcurfn1  24536  preoref22  24561  defse3  24604  dfps2  24621  isdir2  24624  ridlideq  24667  rzrlzreq  24668  grpodivone  24705  rngmgmbs3  24749  rngodmeqrn  24751  zerdivemp1  24768  svs2  24819  islimrs4  24914  bwt2  24924  cnegvex2  24992  rnegvex2  24993  addcanrg  24999  negveud  25000  negveudr  25001  hdrmp  25038  imonclem  25145  isepic  25156  prismorcsetlemc  25249  grphidmor2  25285  cmpmor  25307  pgapspf2  25385  isibcg  25523  zerdivemp1x  25918  bnj545  27939  bnj934  27979  bnj953  27983  dvheveccl  30432
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-cleq 2249
  Copyright terms: Public domain W3C validator