Theorem eqtr 2749

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  sylan9eq  2784  eqvincg  3603  disjeq0  4407  uneqdifeq  4444  propeqop  5450  relresfld  6224  unixpid  6232  fvmptdf  6936  poseq  8091  soseq  8092  eqer  8661  xpider  8715  undifixp  8861  wemaplem2  9439  infeq5  9533  ficard  10459  winalim2  10590  addlsub  11536  pospo  18249  istos  18322  symg2bas  19272  dmatmul  22382  uhgr2edg  29157  clwlkclwwlkf1lem3  29954  eqtrb  32422  bnj545  34878  bnj934  34918  bnj953  34922  ordcmp  36441  bj-snmoore  37107  bj-isclm  37285  bj-bary1lem1  37305  poimirlem26  37646  heicant  37655  ismblfin  37661  volsupnfl  37665  itg2addnclem2  37672  itg2addnc  37674  rngodm1dm2  37932  rngoidmlem  37936  rngo1cl  37939  rngoueqz  37940  zerdivemp1x  37947  disjdmqsss  38800  dvheveccl  41111  rp-isfinite5  43510  clcnvlem  43616  relexpxpmin  43710  gneispace  44127  resipos  48979