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

Theorem eqtr 2460
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 2449 . 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 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436
This theorem is referenced by:  eqtr2  2461  eqtr3  2462  sylan9eq  2495  eqvinc  3101  uneqdifeq  3782  preqsn  4070  relresfld  5379  relcoi1  5381  unixpid  5387  eqer  7149  xpider  7186  undifixp  7314  wemaplem2  7776  infeq5  7858  ficard  8744  winalim2  8878  uzindOLD  10751  pospo  15158  istos  15220  bwthOLD  19029  rngodm1dm2  23920  rngoidmlem  23925  rngo1cl  23931  rngoueqz  23932  zerdivemp1  23936  eqvincg  25874  poseq  27729  soseq  27730  ordcmp  28308  heicant  28445  ismblfin  28451  volsupnfl  28455  itg2addnclem2  28463  itg2addnc  28465  zerdivemp1x  28780  usgra2wlkspthlem1  30315  usgra2adedgspthlem2  30323  dmatmul  30895  bnj545  31907  bnj934  31947  bnj953  31951  bj-lsub  32610  bj-bary1lem1  32619  dvheveccl  34776
  Copyright terms: Public domain W3C validator