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

Theorem eqtr 2483
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 2461 . 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 1395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449
This theorem is referenced by:  eqtr2  2484  eqtr3  2485  sylan9eq  2518  eqvinc  3226  uneqdifeq  3919  preqsn  4215  relresfld  5540  relcoi1  5542  unixpid  5548  eqer  7362  xpider  7400  undifixp  7524  wemaplem2  7990  infeq5  8071  ficard  8957  winalim2  9091  uzindOLD  10978  pospo  15730  istos  15792  symg2bas  16550  dmatmul  19126  usgra2adedgspthlem2  24739  usgra2wlkspthlem1  24746  rngodm1dm2  25547  rngoidmlem  25552  rngo1cl  25558  rngoueqz  25559  zerdivemp1  25563  eqvincg  27501  poseq  29529  soseq  29530  ordcmp  30096  heicant  30233  ismblfin  30239  volsupnfl  30243  itg2addnclem2  30251  itg2addnc  30253  zerdivemp1x  30542  bnj545  34075  bnj934  34115  bnj953  34119  bj-lsub  34793  bj-bary1lem1  34802  dvheveccl  36961  rp-isfinite5  37865
  Copyright terms: Public domain W3C validator