Theorem eqtr 2783

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 2767	. 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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  sylan9eq  2818  eqvincg  3605  disjeq0  4412  uneqdifeq  4451  propeqop  5483  relresfldOLD  6294  unixpid  6302  fvmptdf  7020  mpt3fvot2d  7711  poseq  8199  soseq  8200  eqer  8779  xpider  8834  undifixp  8987  wemaplem2  9565  infeq5  9662  ficard  10673  winalim2  10805  addlsub  11756  pospo  18543  istos  18616  symg2bas  19634  dmatmul  22839  uhgr2edg  29816  clwlkclwwlkf1lem3  30624  eqtrb  33139  bnj545  35592  bnj934  35632  bnj953  35636  mpofvop2d  35796  scottrankeqel  35831  acwer1prclem  35850  ordcmp  37412  bj-snmoore  38224  bj-isclm  38403  bj-bary1lem1  38423  wl-dfcleq  38628  poimirlem26  38755  heicant  38764  ismblfin  38770  volsupnfl  38774  itg2addnclem2  38781  itg2addnc  38783  rngodm1dm2  39057  rngoidmlem  39061  rngo1cl  39064  rngoueqz  39065  zerdivemp1x  39072  disjdmqsss  40028  dvheveccl  42360  rp-isfinite5  44708  clcnvlem  44813  relexpxpmin  44907  gneispace  45324  resipos  50292