Theorem eqtr 2759

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 478	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728

This theorem is referenced by:  eqtr2OLD  2761  eqtr3OLD  2763  sylan9eq  2796  eqvincg  3587  disjeq0  4402  uneqdifeq  4437  propeqop  5451  relresfld  6214  unixpid  6222  fvmptdf  6937  poseq  8045  soseq  8046  eqer  8604  xpider  8648  undifixp  8793  wemaplem2  9404  infeq5  9494  ficard  10422  winalim2  10553  addlsub  11492  pospo  18160  istos  18233  symg2bas  19096  dmatmul  21752  uhgr2edg  27864  clwlkclwwlkf1lem3  28658  eqtrb  31111  bnj545  33174  bnj934  33214  bnj953  33218  ordcmp  34732  bj-snmoore  35389  bj-isclm  35567  bj-bary1lem1  35587  poimirlem26  35908  heicant  35917  ismblfin  35923  volsupnfl  35927  itg2addnclem2  35934  itg2addnc  35936  rngodm1dm2  36195  rngoidmlem  36199  rngo1cl  36202  rngoueqz  36203  zerdivemp1x  36210  disjdmqsss  37069  dvheveccl  39380  rp-isfinite5  41446  clcnvlem  41552  relexpxpmin  41646  gneispace  42065