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

Theorem eqtr 2452
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 2441 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21biimpar 472 1  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652
This theorem is referenced by:  eqtr2  2453  eqtr3  2454  sylan9eq  2487  eqvinc  3055  uneqdifeq  3708  preqsn  3972  relresfld  5387  relcoi1  5389  unixpid  5395  eqer  6929  xpider  6966  undifixp  7089  wemaplem2  7505  infeq5  7581  ficard  8429  winalim2  8560  uzindOLD  10353  pospo  14418  istos  14452  bwth  17461  rngodm1dm2  21994  rngoidmlem  21999  rngo1cl  22005  rngoueqz  22006  zerdivemp1  22010  eqvincg  23949  poseq  25508  soseq  25509  ordcmp  26145  ismblfin  26193  volsupnfl  26197  itg2addnclem2  26203  itg2addnc  26205  zerdivemp1x  26508  usgra2wlkspthlem1  28180  usgra2adedgspthlem2  28188  bnj545  29120  bnj934  29160  bnj953  29164  dvheveccl  31749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator