Theorem eqtr 2751

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

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

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 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  sylan9eq  2786  eqvincg  3598  disjeq0  4403  uneqdifeq  4440  propeqop  5445  relresfld  6223  unixpid  6231  fvmptdf  6935  poseq  8088  soseq  8089  eqer  8658  xpider  8712  undifixp  8858  wemaplem2  9433  infeq5  9527  ficard  10456  winalim2  10587  addlsub  11533  pospo  18249  istos  18322  symg2bas  19305  dmatmul  22412  uhgr2edg  29186  clwlkclwwlkf1lem3  29986  eqtrb  32453  bnj545  34907  bnj934  34947  bnj953  34951  ordcmp  36491  bj-snmoore  37157  bj-isclm  37335  bj-bary1lem1  37355  poimirlem26  37685  heicant  37694  ismblfin  37700  volsupnfl  37704  itg2addnclem2  37711  itg2addnc  37713  rngodm1dm2  37971  rngoidmlem  37975  rngo1cl  37978  rngoueqz  37979  zerdivemp1x  37986  disjdmqsss  38899  dvheveccl  41210  rp-isfinite5  43609  clcnvlem  43715  relexpxpmin  43809  gneispace  44226  resipos  49074