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

Theorem eqtr 2270
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 2259 . 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  2271  eqtr3  2272  sylan9eq  2305  eqvinc  2832  uneqdifeq  3448  preqsn  3692  relresfld  5105  relcoi1  5107  unixpid  5113  eqer  6579  xpider  6616  undifixp  6738  wemaplem2  7146  infeq5  7222  ficard  8069  winalim2  8198  uzindOLD  9985  pospo  13951  istos  13985  rngodm1dm2  20915  rngoidmlem  20920  rngo1cl  20926  rngoueqz  20927  poseq  23421  soseq  23422  elfuns  23628  ordcmp  24060  neiopne  24216  oooeqim2  24218  domfldref  24226  rnintintrn  24292  sssu  24307  injsurinj  24315  repfuntw  24326  cbcpcp  24328  jidd  24358  midd  24359  valcurfn1  24370  preoref22  24395  defse3  24438  dfps2  24455  isdir2  24458  ridlideq  24501  rzrlzreq  24502  grpodivone  24539  rngmgmbs3  24583  rngodmeqrn  24585  zerdivemp1  24602  svs2  24653  islimrs4  24748  bwt2  24758  cnegvex2  24826  rnegvex2  24827  addcanrg  24833  negveud  24834  negveudr  24835  hdrmp  24872  imonclem  24979  isepic  24990  prismorcsetlemc  25083  grphidmor2  25119  cmpmor  25141  pgapspf2  25219  isibcg  25357  zerdivemp1x  25752  bnj545  27616  bnj934  27656  bnj953  27660  dvheveccl  29991
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 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-cleq 2246
  Copyright terms: Public domain W3C validator