Theorem eqtr 2750

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 2734	. 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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  sylan9eq  2785  eqvincg  3617  disjeq0  4422  uneqdifeq  4459  propeqop  5470  relresfld  6252  unixpid  6260  fvmptdf  6977  poseq  8140  soseq  8141  eqer  8710  xpider  8764  undifixp  8910  wemaplem2  9507  infeq5  9597  ficard  10525  winalim2  10656  addlsub  11601  pospo  18311  istos  18384  symg2bas  19330  dmatmul  22391  uhgr2edg  29142  clwlkclwwlkf1lem3  29942  eqtrb  32410  bnj545  34892  bnj934  34932  bnj953  34936  ordcmp  36442  bj-snmoore  37108  bj-isclm  37286  bj-bary1lem1  37306  poimirlem26  37647  heicant  37656  ismblfin  37662  volsupnfl  37666  itg2addnclem2  37673  itg2addnc  37675  rngodm1dm2  37933  rngoidmlem  37937  rngo1cl  37940  rngoueqz  37941  zerdivemp1x  37948  disjdmqsss  38801  dvheveccl  41113  rp-isfinite5  43513  clcnvlem  43619  relexpxpmin  43713  gneispace  44130  resipos  48967