Theorem eqtr 2786

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758

This theorem is used by:  sylan9eq  2821  eqvincg  3610  disjeq0  4419  uneqdifeq  4456  propeqop  5493  relresfld  6281  unixpid  6289  fvmptdf  7000  poseq  8156  soseq  8157  eqer  8733  xpider  8788  undifixp  8934  wemaplem2  9511  infeq5  9608  ficard  10559  winalim2  10691  addlsub  11640  pospo  18409  istos  18482  symg2bas  19473  dmatmul  22669  uhgr2edg  29573  clwlkclwwlkf1lem3  30372  eqtrb  32835  bnj545  35296  bnj934  35336  bnj953  35340  scottrankeqel  35530  ordcmp  36990  bj-snmoore  37787  bj-isclm  37967  bj-bary1lem1  37987  wl-dfcleq  38192  poimirlem26  38329  heicant  38338  ismblfin  38344  volsupnfl  38348  itg2addnclem2  38355  itg2addnc  38357  rngodm1dm2  38615  rngoidmlem  38619  rngo1cl  38622  rngoueqz  38623  zerdivemp1x  38630  disjdmqsss  39586  dvheveccl  41918  rp-isfinite5  44275  clcnvlem  44381  relexpxpmin  44475  gneispace  44892  resipos  49785