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

Theorem eqtr 2493
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 2471 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21biimpar 485 1  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459
This theorem is referenced by:  eqtr2  2494  eqtr3  2495  sylan9eq  2528  eqvinc  3230  uneqdifeq  3915  preqsn  4209  relresfld  5534  relcoi1  5536  unixpid  5542  eqer  7344  xpider  7382  undifixp  7505  wemaplem2  7972  infeq5  8054  ficard  8940  winalim2  9074  uzindOLD  10955  pospo  15460  istos  15522  dmatmul  18794  bwthOLD  19705  usgra2adedgspthlem2  24316  usgra2wlkspthlem1  24323  rngodm1dm2  25124  rngoidmlem  25129  rngo1cl  25135  rngoueqz  25136  zerdivemp1  25140  eqvincg  27078  poseq  28938  soseq  28939  ordcmp  29517  heicant  29654  ismblfin  29660  volsupnfl  29664  itg2addnclem2  29672  itg2addnc  29674  zerdivemp1x  29989  bnj545  33050  bnj934  33090  bnj953  33094  bj-lsub  33761  bj-bary1lem1  33770  dvheveccl  35927
  Copyright terms: Public domain W3C validator