Theorem eqtr 2761

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

Step	Hyp	Ref	Expression
1		eqeq1 2742	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpar 478	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = 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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  eqtr2OLD  2763  eqtr3OLD  2765  sylan9eq  2798  eqvincg  3578  disjeq0  4389  uneqdifeq  4423  propeqop  5421  relresfld  6179  unixpid  6187  fvmptdf  6881  eqer  8533  xpider  8577  undifixp  8722  wemaplem2  9306  infeq5  9395  ficard  10321  winalim2  10452  addlsub  11391  pospo  18063  istos  18136  symg2bas  19000  dmatmul  21646  uhgr2edg  27575  clwlkclwwlkf1lem3  28370  eqtrb  30823  bnj545  32875  bnj934  32915  bnj953  32919  poseq  33802  soseq  33803  ordcmp  34636  bj-snmoore  35284  bj-isclm  35462  bj-bary1lem1  35482  poimirlem26  35803  heicant  35812  ismblfin  35818  volsupnfl  35822  itg2addnclem2  35829  itg2addnc  35831  rngodm1dm2  36090  rngoidmlem  36094  rngo1cl  36097  rngoueqz  36098  zerdivemp1x  36105  dvheveccl  39126  rp-isfinite5  41124  clcnvlem  41231  relexpxpmin  41325  gneispace  41744