Theorem eqtr 2755

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  sylan9eq  2790  eqvincg  3627  disjeq0  4431  uneqdifeq  4468  propeqop  5482  relresfld  6265  unixpid  6273  fvmptdf  6992  poseq  8157  soseq  8158  eqer  8755  xpider  8802  undifixp  8948  wemaplem2  9561  infeq5  9651  ficard  10579  winalim2  10710  addlsub  11653  pospo  18355  istos  18428  symg2bas  19374  dmatmul  22435  uhgr2edg  29187  clwlkclwwlkf1lem3  29987  eqtrb  32455  bnj545  34926  bnj934  34966  bnj953  34970  ordcmp  36465  bj-snmoore  37131  bj-isclm  37309  bj-bary1lem1  37329  poimirlem26  37670  heicant  37679  ismblfin  37685  volsupnfl  37689  itg2addnclem2  37696  itg2addnc  37698  rngodm1dm2  37956  rngoidmlem  37960  rngo1cl  37963  rngoueqz  37964  zerdivemp1x  37971  disjdmqsss  38820  dvheveccl  41131  rp-isfinite5  43541  clcnvlem  43647  relexpxpmin  43741  gneispace  44158  resipos  48949