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

Theorem eqtr 2818
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 2803 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21biimpar 470 1 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385   = wceq 1653
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2792
This theorem is referenced by:  eqtr2  2819  eqtr3  2820  sylan9eq  2853  eqvincg  3518  disjeq0  4218  uneqdifeq  4251  propeqop  5163  relresfld  5881  unixpid  5889  eqer  8017  xpider  8056  undifixp  8184  wemaplem2  8694  infeq5  8784  ficard  9675  winalim2  9806  addlsub  10739  pospo  17288  istos  17350  symg2bas  18130  dmatmul  20629  uhgr2edg  26441  clwlkclwwlkf1lem3  27302  clwlkclwwlkf1lem3OLD  27303  bnj545  31482  bnj934  31522  bnj953  31526  poseq  32266  soseq  32267  ordcmp  32954  bj-snmoore  33561  bj-bary1lem1  33660  poimirlem26  33924  heicant  33933  ismblfin  33939  volsupnfl  33943  itg2addnclem2  33950  itg2addnc  33952  rngodm1dm2  34218  rngoidmlem  34222  rngo1cl  34225  rngoueqz  34226  zerdivemp1x  34233  dvheveccl  37133  rp-isfinite5  38646  clcnvlem  38713  relexpxpmin  38792  gneispace  39214
  Copyright terms: Public domain W3C validator