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

Theorem eqtr 2628
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 2613 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21biimpar 500 1 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602
This theorem is referenced by:  eqtr2  2629  eqtr3  2630  sylan9eq  2663  eqvinc  3299  uneqdifeq  4008  uneqdifeqOLD  4009  preqsnOLD  4327  relresfld  5565  unixpid  5573  eqer  7641  eqerOLD  7642  xpider  7682  undifixp  7807  wemaplem2  8312  infeq5  8394  ficard  9243  winalim2  9374  addlsub  10298  pospo  16742  istos  16804  symg2bas  17587  dmatmul  20064  usgra2adedgspthlem2  25906  usgra2wlkspthlem1  25913  eqvincg  28504  bnj545  30025  bnj934  30065  bnj953  30069  poseq  30800  soseq  30801  ordcmp  31422  bj-bary1lem1  32134  poimirlem26  32401  heicant  32410  ismblfin  32416  volsupnfl  32420  itg2addnclem2  32428  itg2addnc  32430  rngodm1dm2  32697  rngoidmlem  32701  rngo1cl  32704  rngoueqz  32705  zerdivemp1x  32712  dvheveccl  35215  rp-isfinite5  36678  clcnvlem  36745  relexpxpmin  36824  gneispace  37248  propeqop  40119  uhgr2edg  40430
  Copyright terms: Public domain W3C validator