Theorem eqtr 2749

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540

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 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  sylan9eq  2784  eqvincg  3611  disjeq0  4415  uneqdifeq  4452  propeqop  5462  relresfld  6237  unixpid  6245  fvmptdf  6956  poseq  8114  soseq  8115  eqer  8684  xpider  8738  undifixp  8884  wemaplem2  9476  infeq5  9568  ficard  10496  winalim2  10627  addlsub  11572  pospo  18285  istos  18358  symg2bas  19308  dmatmul  22418  uhgr2edg  29189  clwlkclwwlkf1lem3  29986  eqtrb  32454  bnj545  34879  bnj934  34919  bnj953  34923  ordcmp  36429  bj-snmoore  37095  bj-isclm  37273  bj-bary1lem1  37293  poimirlem26  37634  heicant  37643  ismblfin  37649  volsupnfl  37653  itg2addnclem2  37660  itg2addnc  37662  rngodm1dm2  37920  rngoidmlem  37924  rngo1cl  37927  rngoueqz  37928  zerdivemp1x  37935  disjdmqsss  38788  dvheveccl  41100  rp-isfinite5  43500  clcnvlem  43606  relexpxpmin  43700  gneispace  44117  resipos  48957