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

Theorem eqtr 2670
 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 2655 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21biimpar 501 1 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644 This theorem is referenced by:  eqtr2  2671  eqtr3  2672  sylan9eq  2705  eqvincg  3360  uneqdifeq  4090  uneqdifeqOLD  4091  preqsnOLD  4425  propeqop  4999  relresfld  5700  unixpid  5708  eqer  7822  xpider  7861  undifixp  7986  wemaplem2  8493  infeq5  8572  ficard  9425  winalim2  9556  addlsub  10485  pospo  17020  istos  17082  symg2bas  17864  dmatmul  20351  uhgr2edg  26145  bnj545  31091  bnj934  31131  bnj953  31135  poseq  31878  soseq  31879  ordcmp  32571  bj-snmoore  33193  bj-bary1lem1  33291  poimirlem26  33565  heicant  33574  ismblfin  33580  volsupnfl  33584  itg2addnclem2  33592  itg2addnc  33594  rngodm1dm2  33861  rngoidmlem  33865  rngo1cl  33868  rngoueqz  33869  zerdivemp1x  33876  dvheveccl  36718  rp-isfinite5  38180  clcnvlem  38247  relexpxpmin  38326  gneispace  38749
 Copyright terms: Public domain W3C validator