Theorem eqtr 2840

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536

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 1969  ax-7 2014  ax-9 2123  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2813

This theorem is referenced by:  eqtr2  2841  eqtr3  2842  sylan9eq  2875  eqvincg  3640  disjeq0  4402  uneqdifeq  4435  propeqop  5394  relresfld  6124  unixpid  6132  fvmptdf  6771  eqer  8321  xpider  8365  undifixp  8495  wemaplem2  9008  infeq5  9097  ficard  9984  winalim2  10115  addlsub  11053  pospo  17579  istos  17641  symg2bas  18517  dmatmul  21102  uhgr2edg  26988  clwlkclwwlkf1lem3  27782  eqtrb  30236  bnj545  32191  bnj934  32231  bnj953  32235  poseq  33119  soseq  33120  ordcmp  33819  bj-snmoore  34432  bj-isclm  34599  bj-bary1lem1  34619  poimirlem26  34956  heicant  34965  ismblfin  34971  volsupnfl  34975  itg2addnclem2  34982  itg2addnc  34984  rngodm1dm2  35246  rngoidmlem  35250  rngo1cl  35253  rngoueqz  35254  zerdivemp1x  35261  dvheveccl  38284  rp-isfinite5  39957  clcnvlem  40057  relexpxpmin  40136  gneispace  40558