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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733

This theorem is referenced by:  sylan9eq  2796  eqvincg  3588  disjeq0  4387  uneqdifeq  4423  propeqop  5451  relresfld  6231  unixpid  6239  fvmptdf  6946  poseq  8102  soseq  8103  eqer  8674  xpider  8729  undifixp  8876  wemaplem2  9456  infeq5  9553  ficard  10482  winalim2  10614  addlsub  11561  pospo  18304  istos  18377  symg2bas  19363  dmatmul  22484  uhgr2edg  29299  clwlkclwwlkf1lem3  30098  eqtrb  32565  bnj545  35092  bnj934  35132  bnj953  35136  ordcmp  36690  bj-snmoore  37486  bj-isclm  37666  bj-bary1lem1  37686  wl-dfcleq  37891  poimirlem26  38028  heicant  38037  ismblfin  38043  volsupnfl  38047  itg2addnclem2  38054  itg2addnc  38056  rngodm1dm2  38314  rngoidmlem  38318  rngo1cl  38321  rngoueqz  38322  zerdivemp1x  38329  disjdmqsss  39287  dvheveccl  41619  rp-isfinite5  43976  clcnvlem  44082  relexpxpmin  44176  gneispace  44593  resipos  49479