Theorem eqtr 2782

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754

This theorem is used by:  sylan9eq  2817  eqvincg  3606  disjeq0  4415  uneqdifeq  4452  propeqop  5489  relresfld  6277  unixpid  6285  fvmptdf  6996  poseq  8152  soseq  8153  eqer  8729  xpider  8784  undifixp  8930  wemaplem2  9507  infeq5  9604  ficard  10555  winalim2  10687  addlsub  11636  pospo  18405  istos  18478  symg2bas  19469  dmatmul  22665  uhgr2edg  29569  clwlkclwwlkf1lem3  30368  eqtrb  32831  bnj545  35292  bnj934  35332  bnj953  35336  scottrankeqel  35526  ordcmp  36986  bj-snmoore  37783  bj-isclm  37963  bj-bary1lem1  37983  wl-dfcleq  38188  poimirlem26  38325  heicant  38334  ismblfin  38340  volsupnfl  38344  itg2addnclem2  38351  itg2addnc  38353  rngodm1dm2  38611  rngoidmlem  38615  rngo1cl  38618  rngoueqz  38619  zerdivemp1x  38626  disjdmqsss  39582  dvheveccl  41914  rp-isfinite5  44271  clcnvlem  44377  relexpxpmin  44471  gneispace  44888  resipos  49781