Theorem eqtr 2629

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603

This theorem is referenced by:  eqtr2  2630  eqtr3  2631  sylan9eq  2664  eqvinc  3300  uneqdifeq  4009  uneqdifeqOLD  4010  preqsnOLD  4332  propeqop  4895  relresfld  5579  unixpid  5587  eqer  7664  eqerOLD  7665  xpider  7705  undifixp  7830  wemaplem2  8335  infeq5  8417  ficard  9266  winalim2  9397  addlsub  10326  pospo  16796  istos  16858  symg2bas  17641  dmatmul  20122  usgra2adedgspthlem2  26140  usgra2wlkspthlem1  26147  eqvincg  28698  bnj545  30219  bnj934  30259  bnj953  30263  poseq  30994  soseq  30995  ordcmp  31616  bj-bary1lem1  32338  poimirlem26  32605  heicant  32614  ismblfin  32620  volsupnfl  32624  itg2addnclem2  32632  itg2addnc  32634  rngodm1dm2  32901  rngoidmlem  32905  rngo1cl  32908  rngoueqz  32909  zerdivemp1x  32916  dvheveccl  35419  rp-isfinite5  36882  clcnvlem  36949  relexpxpmin  37028  gneispace  37452  uhgr2edg  40435