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

Theorem eqtr 2779
 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 2763 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21biimpar 482 1 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539 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 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751 This theorem is referenced by:  eqtr2  2780  eqtr3  2781  sylan9eq  2814  eqvincg  3560  disjeq0  4353  uneqdifeq  4387  propeqop  5367  relresfld  6106  unixpid  6114  fvmptdf  6766  eqer  8335  xpider  8379  undifixp  8517  wemaplem2  9037  infeq5  9126  ficard  10018  winalim2  10149  addlsub  11087  pospo  17642  istos  17704  symg2bas  18581  dmatmul  21190  uhgr2edg  27090  clwlkclwwlkf1lem3  27883  eqtrb  30337  bnj545  32388  bnj934  32428  bnj953  32432  poseq  33349  soseq  33350  ordcmp  34178  bj-snmoore  34801  bj-isclm  34978  bj-bary1lem1  34998  poimirlem26  35356  heicant  35365  ismblfin  35371  volsupnfl  35375  itg2addnclem2  35382  itg2addnc  35384  rngodm1dm2  35643  rngoidmlem  35647  rngo1cl  35650  rngoueqz  35651  zerdivemp1x  35658  dvheveccl  38681  rp-isfinite5  40591  clcnvlem  40689  relexpxpmin  40784  gneispace  41203
 Copyright terms: Public domain W3C validator