Theorem eqtr 2757

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  sylan9eq  2792  eqvincg  3603  disjeq0  4409  uneqdifeq  4446  propeqop  5456  relresfld  6235  unixpid  6243  fvmptdf  6949  poseq  8102  soseq  8103  eqer  8674  xpider  8729  undifixp  8876  wemaplem2  9456  infeq5  9550  ficard  10479  winalim2  10611  addlsub  11557  pospo  18270  istos  18343  symg2bas  19326  dmatmul  22445  uhgr2edg  29285  clwlkclwwlkf1lem3  30085  eqtrb  32551  bnj545  35053  bnj934  35093  bnj953  35097  ordcmp  36643  bj-snmoore  37320  bj-isclm  37498  bj-bary1lem1  37518  poimirlem26  37849  heicant  37858  ismblfin  37864  volsupnfl  37868  itg2addnclem2  37875  itg2addnc  37877  rngodm1dm2  38135  rngoidmlem  38139  rngo1cl  38142  rngoueqz  38143  zerdivemp1x  38150  disjdmqsss  39108  dvheveccl  41440  rp-isfinite5  43825  clcnvlem  43931  relexpxpmin  44025  gneispace  44442  resipos  49287