Theorem eqtr 2761

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqtr2OLD  2763  eqtr3OLD  2765  sylan9eq  2799  eqvincg  3570  disjeq0  4386  uneqdifeq  4420  propeqop  5415  relresfld  6168  unixpid  6176  fvmptdf  6863  eqer  8491  xpider  8535  undifixp  8680  wemaplem2  9236  infeq5  9325  ficard  10252  winalim2  10383  addlsub  11321  pospo  17978  istos  18051  symg2bas  18915  dmatmul  21554  uhgr2edg  27478  clwlkclwwlkf1lem3  28271  eqtrb  30724  bnj545  32775  bnj934  32815  bnj953  32819  poseq  33729  soseq  33730  ordcmp  34563  bj-snmoore  35211  bj-isclm  35389  bj-bary1lem1  35409  poimirlem26  35730  heicant  35739  ismblfin  35745  volsupnfl  35749  itg2addnclem2  35756  itg2addnc  35758  rngodm1dm2  36017  rngoidmlem  36021  rngo1cl  36024  rngoueqz  36025  zerdivemp1x  36032  dvheveccl  39053  rp-isfinite5  41022  clcnvlem  41120  relexpxpmin  41214  gneispace  41633