Theorem eqtr 2628

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602

This theorem is referenced by:  eqtr2  2629  eqtr3  2630  sylan9eq  2663  eqvinc  3299  uneqdifeq  4008  uneqdifeqOLD  4009  preqsnOLD  4327  relresfld  5565  unixpid  5573  eqer  7641  eqerOLD  7642  xpider  7682  undifixp  7807  wemaplem2  8312  infeq5  8394  ficard  9243  winalim2  9374  addlsub  10298  pospo  16742  istos  16804  symg2bas  17587  dmatmul  20064  usgra2adedgspthlem2  25906  usgra2wlkspthlem1  25913  eqvincg  28504  bnj545  30025  bnj934  30065  bnj953  30069  poseq  30800  soseq  30801  ordcmp  31422  bj-bary1lem1  32134  poimirlem26  32401  heicant  32410  ismblfin  32416  volsupnfl  32420  itg2addnclem2  32428  itg2addnc  32430  rngodm1dm2  32697  rngoidmlem  32701  rngo1cl  32704  rngoueqz  32705  zerdivemp1x  32712  dvheveccl  35215  rp-isfinite5  36678  clcnvlem  36745  relexpxpmin  36824  gneispace  37248  propeqop  40119  uhgr2edg  40430