Theorem eqtr 2784

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756

This theorem is referenced by:  sylan9eq  2819  eqvincg  3609  disjeq0  4412  uneqdifeq  4448  propeqop  5478  relresfld  6265  unixpid  6273  fvmptdf  6984  poseq  8140  soseq  8141  eqer  8717  xpider  8772  undifixp  8918  wemaplem2  9497  infeq5  9594  ficard  10524  winalim2  10656  addlsub  11605  pospo  18377  istos  18450  symg2bas  19435  dmatmul  22559  uhgr2edg  29411  clwlkclwwlkf1lem3  30210  eqtrb  32675  bnj545  35192  bnj934  35232  bnj953  35236  ordcmp  36812  bj-snmoore  37608  bj-isclm  37788  bj-bary1lem1  37808  wl-dfcleq  38013  poimirlem26  38150  heicant  38159  ismblfin  38165  volsupnfl  38169  itg2addnclem2  38176  itg2addnc  38178  rngodm1dm2  38436  rngoidmlem  38440  rngo1cl  38443  rngoueqz  38444  zerdivemp1x  38451  disjdmqsss  39409  dvheveccl  41741  rp-isfinite5  44098  clcnvlem  44204  relexpxpmin  44298  gneispace  44715  resipos  49601