Theorem eqtr 2780

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  sylan9eq  2815  eqvincg  3601  disjeq0  4408  uneqdifeq  4447  propeqop  5478  relresfldOLD  6279  unixpid  6287  fvmptdf  7000  mpt3fvot2d  7690  poseq  8175  soseq  8176  eqer  8754  xpider  8809  undifixp  8962  wemaplem2  9541  infeq5  9638  ficard  10649  winalim2  10781  addlsub  11732  pospo  18517  istos  18590  symg2bas  19607  dmatmul  22812  uhgr2edg  29789  clwlkclwwlkf1lem3  30597  eqtrb  33070  bnj545  35525  bnj934  35565  bnj953  35569  scottrankeqel  35748  acwer1prclem  35759  ordcmp  37235  bj-snmoore  38034  bj-isclm  38213  bj-bary1lem1  38233  wl-dfcleq  38438  poimirlem26  38565  heicant  38574  ismblfin  38580  volsupnfl  38584  itg2addnclem2  38591  itg2addnc  38593  rngodm1dm2  38867  rngoidmlem  38871  rngo1cl  38874  rngoueqz  38875  zerdivemp1x  38882  disjdmqsss  39838  dvheveccl  42170  rp-isfinite5  44518  clcnvlem  44623  relexpxpmin  44717  gneispace  45134  resipos  50083