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

Theorem eqtr 2838
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 2822 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21biimpar 478 1 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  eqtr2  2839  eqtr3  2840  sylan9eq  2873  eqvincg  3638  disjeq0  4401  uneqdifeq  4434  propeqop  5388  relresfld  6120  unixpid  6128  eqer  8313  xpider  8357  undifixp  8486  wemaplem2  8999  infeq5  9088  ficard  9975  winalim2  10106  addlsub  11044  pospo  17571  istos  17633  symg2bas  18455  dmatmul  21034  uhgr2edg  26917  clwlkclwwlkf1lem3  27711  eqtrb  30165  bnj545  32066  bnj934  32106  bnj953  32110  poseq  32992  soseq  32993  ordcmp  33692  bj-snmoore  34299  bj-isclm  34460  bj-bary1lem1  34480  poimirlem26  34799  heicant  34808  ismblfin  34814  volsupnfl  34818  itg2addnclem2  34825  itg2addnc  34827  rngodm1dm2  35091  rngoidmlem  35095  rngo1cl  35098  rngoueqz  35099  zerdivemp1x  35106  dvheveccl  38128  rp-isfinite5  39761  clcnvlem  39861  relexpxpmin  39940  gneispace  40362
  Copyright terms: Public domain W3C validator