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

Theorem eqtr 2481
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 2466 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21biimpar 492 1  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-cleq 2455
This theorem is referenced by:  eqtr2  2482  eqtr3  2483  sylan9eq  2516  eqvinc  3178  uneqdifeq  3868  preqsn  4173  relresfld  5381  relcoi1OLD  5384  unixpid  5390  eqer  7422  xpider  7460  undifixp  7584  wemaplem2  8088  infeq5  8168  ficard  9016  winalim2  9147  addlsub  10064  pospo  16268  istos  16330  symg2bas  17088  dmatmul  19571  usgra2adedgspthlem2  25389  usgra2wlkspthlem1  25396  rngodm1dm2  26195  rngoidmlem  26200  rngo1cl  26206  rngoueqz  26207  zerdivemp1  26211  eqvincg  28157  bnj545  29755  bnj934  29795  bnj953  29799  poseq  30540  soseq  30541  ordcmp  31156  bj-bary1lem1  31761  poimirlem26  32011  heicant  32020  ismblfin  32026  volsupnfl  32030  itg2addnclem2  32039  itg2addnc  32041  zerdivemp1x  32239  dvheveccl  34725  rp-isfinite5  36207  clcnvlem  36275  relexpxpmin  36354  propeqop  39039  uhgr2edg  39339
  Copyright terms: Public domain W3C validator