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

Theorem eqtr 2756
Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
Assertion
Ref Expression
eqtr ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)

Proof of Theorem eqtr
StepHypRef Expression
1 eqeq1 2737 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21biimpar 479 1 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725
This theorem is referenced by:  eqtr2OLD  2758  eqtr3OLD  2760  sylan9eq  2793  eqvincg  3602  disjeq0  4419  uneqdifeq  4454  propeqop  5468  relresfld  6232  unixpid  6240  fvmptdf  6958  poseq  8094  soseq  8095  eqer  8689  xpider  8733  undifixp  8878  wemaplem2  9491  infeq5  9581  ficard  10509  winalim2  10640  addlsub  11579  pospo  18242  istos  18315  symg2bas  19182  dmatmul  21869  uhgr2edg  28205  clwlkclwwlkf1lem3  28999  eqtrb  31452  bnj545  33571  bnj934  33611  bnj953  33615  ordcmp  34972  bj-snmoore  35634  bj-isclm  35812  bj-bary1lem1  35832  poimirlem26  36154  heicant  36163  ismblfin  36169  volsupnfl  36173  itg2addnclem2  36180  itg2addnc  36182  rngodm1dm2  36441  rngoidmlem  36445  rngo1cl  36448  rngoueqz  36449  zerdivemp1x  36456  disjdmqsss  37314  dvheveccl  39625  rp-isfinite5  41881  clcnvlem  41987  relexpxpmin  42081  gneispace  42498
  Copyright terms: Public domain W3C validator