Theorem eqtr 2756

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  sylan9eq  2791  eqvincg  3590  disjeq0  4396  uneqdifeq  4432  propeqop  5461  relresfld  6240  unixpid  6248  fvmptdf  6954  poseq  8108  soseq  8109  eqer  8680  xpider  8735  undifixp  8882  wemaplem2  9462  infeq5  9558  ficard  10487  winalim2  10619  addlsub  11566  pospo  18309  istos  18382  symg2bas  19368  dmatmul  22462  uhgr2edg  29277  clwlkclwwlkf1lem3  30076  eqtrb  32543  bnj545  35037  bnj934  35077  bnj953  35081  ordcmp  36629  bj-snmoore  37425  bj-isclm  37605  bj-bary1lem1  37625  wl-dfcleq  37830  poimirlem26  37967  heicant  37976  ismblfin  37982  volsupnfl  37986  itg2addnclem2  37993  itg2addnc  37995  rngodm1dm2  38253  rngoidmlem  38257  rngo1cl  38260  rngoueqz  38261  zerdivemp1x  38268  disjdmqsss  39226  dvheveccl  41558  rp-isfinite5  43944  clcnvlem  44050  relexpxpmin  44144  gneispace  44561  resipos  49450