Theorem eqtr 2753

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqtr2OLD  2755  eqtr3OLD  2757  sylan9eq  2790  eqvincg  3637  disjeq0  4456  uneqdifeq  4493  propeqop  5508  relresfld  6276  unixpid  6284  fvmptdf  7005  poseq  8148  soseq  8149  eqer  8742  xpider  8786  undifixp  8932  wemaplem2  9546  infeq5  9636  ficard  10564  winalim2  10695  addlsub  11636  pospo  18304  istos  18377  symg2bas  19303  dmatmul  22221  uhgr2edg  28730  clwlkclwwlkf1lem3  29524  eqtrb  31979  bnj545  34202  bnj934  34242  bnj953  34246  ordcmp  35637  bj-snmoore  36299  bj-isclm  36477  bj-bary1lem1  36497  poimirlem26  36819  heicant  36828  ismblfin  36834  volsupnfl  36838  itg2addnclem2  36845  itg2addnc  36847  rngodm1dm2  37105  rngoidmlem  37109  rngo1cl  37112  rngoueqz  37113  zerdivemp1x  37120  disjdmqsss  37977  dvheveccl  40288  rp-isfinite5  42572  clcnvlem  42678  relexpxpmin  42772  gneispace  43189