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

Theorem eqtr 2275
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 2264 . 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  2276  eqtr3  2277  sylan9eq  2310  eqvinc  2870  uneqdifeq  3517  preqsn  3766  relresfld  5186  relcoi1  5188  unixpid  5194  eqer  6661  xpider  6698  undifixp  6820  wemaplem2  7230  infeq5  7306  ficard  8155  winalim2  8286  uzindOLD  10073  pospo  14069  istos  14103  rngodm1dm2  21045  rngoidmlem  21050  rngo1cl  21056  rngoueqz  21057  poseq  23622  soseq  23623  elfuns  23829  ordcmp  24261  neiopne  24417  oooeqim2  24419  domfldref  24427  rnintintrn  24493  sssu  24508  injsurinj  24516  repfuntw  24527  cbcpcp  24529  jidd  24559  midd  24560  valcurfn1  24571  preoref22  24596  defse3  24639  dfps2  24656  isdir2  24659  ridlideq  24702  rzrlzreq  24703  grpodivone  24740  rngmgmbs3  24784  rngodmeqrn  24786  zerdivemp1  24803  svs2  24854  islimrs4  24949  bwt2  24959  cnegvex2  25027  rnegvex2  25028  addcanrg  25034  negveud  25035  negveudr  25036  hdrmp  25073  imonclem  25180  isepic  25191  prismorcsetlemc  25284  grphidmor2  25320  cmpmor  25342  pgapspf2  25420  isibcg  25558  zerdivemp1x  25953  bnj545  27976  bnj934  28016  bnj953  28020  dvheveccl  30469
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 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-cleq 2251
  Copyright terms: Public domain W3C validator