Theorem eqtr 2816

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 2799	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpar 478	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788

This theorem is referenced by:  eqtr2  2817  eqtr3  2818  sylan9eq  2851  eqvincg  3580  disjeq0  4319  uneqdifeq  4352  propeqop  5288  relresfld  6002  unixpid  6010  eqer  8174  xpider  8218  undifixp  8346  wemaplem2  8857  infeq5  8946  ficard  9833  winalim2  9964  addlsub  10904  pospo  17412  istos  17474  symg2bas  18257  dmatmul  20790  uhgr2edg  26673  clwlkclwwlkf1lem3  27471  eqtrb  29930  bnj545  31783  bnj934  31823  bnj953  31827  poseq  32705  soseq  32706  ordcmp  33405  bj-snmoore  34024  bj-bary1lem1  34148  poimirlem26  34468  heicant  34477  ismblfin  34483  volsupnfl  34487  itg2addnclem2  34494  itg2addnc  34496  rngodm1dm2  34761  rngoidmlem  34765  rngo1cl  34768  rngoueqz  34769  zerdivemp1x  34776  dvheveccl  37798  rp-isfinite5  39387  clcnvlem  39487  relexpxpmin  39566  gneispace  39988