Theorem eqtr 2763

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqtr2OLD  2765  eqtr3OLD  2767  sylan9eq  2800  eqvincg  3661  disjeq0  4479  uneqdifeq  4516  propeqop  5526  relresfld  6307  unixpid  6315  fvmptdf  7035  poseq  8199  soseq  8200  eqer  8799  xpider  8846  undifixp  8992  wemaplem2  9616  infeq5  9706  ficard  10634  winalim2  10765  addlsub  11706  pospo  18415  istos  18488  symg2bas  19434  dmatmul  22524  uhgr2edg  29243  clwlkclwwlkf1lem3  30038  eqtrb  32502  bnj545  34871  bnj934  34911  bnj953  34915  ordcmp  36413  bj-snmoore  37079  bj-isclm  37257  bj-bary1lem1  37277  poimirlem26  37606  heicant  37615  ismblfin  37621  volsupnfl  37625  itg2addnclem2  37632  itg2addnc  37634  rngodm1dm2  37892  rngoidmlem  37896  rngo1cl  37899  rngoueqz  37900  zerdivemp1x  37907  disjdmqsss  38758  dvheveccl  41069  rp-isfinite5  43479  clcnvlem  43585  relexpxpmin  43679  gneispace  44096