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  3614  disjeq0  4419  uneqdifeq  4456  propeqop  5467  relresfld  6249  unixpid  6257  fvmptdf  6974  poseq  8137  soseq  8138  eqer  8707  xpider  8761  undifixp  8907  wemaplem2  9500  infeq5  9590  ficard  10518  winalim2  10649  addlsub  11594  pospo  18304  istos  18377  symg2bas  19323  dmatmul  22384  uhgr2edg  29135  clwlkclwwlkf1lem3  29935  eqtrb  32403  bnj545  34885  bnj934  34925  bnj953  34929  ordcmp  36435  bj-snmoore  37101  bj-isclm  37279  bj-bary1lem1  37299  poimirlem26  37640  heicant  37649  ismblfin  37655  volsupnfl  37659  itg2addnclem2  37666  itg2addnc  37668  rngodm1dm2  37926  rngoidmlem  37930  rngo1cl  37933  rngoueqz  37934  zerdivemp1x  37941  disjdmqsss  38794  dvheveccl  41106  rp-isfinite5  43506  clcnvlem  43612  relexpxpmin  43706  gneispace  44123  resipos  48963