Theorem eqtr 2818

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

Syntax hints:   → wi 4   ∧ wa 385   = wceq 1653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2792

This theorem is referenced by:  eqtr2  2819  eqtr3  2820  sylan9eq  2853  eqvincg  3518  disjeq0  4218  uneqdifeq  4251  propeqop  5163  relresfld  5881  unixpid  5889  eqer  8017  xpider  8056  undifixp  8184  wemaplem2  8694  infeq5  8784  ficard  9675  winalim2  9806  addlsub  10739  pospo  17288  istos  17350  symg2bas  18130  dmatmul  20629  uhgr2edg  26441  clwlkclwwlkf1lem3  27302  clwlkclwwlkf1lem3OLD  27303  bnj545  31482  bnj934  31522  bnj953  31526  poseq  32266  soseq  32267  ordcmp  32954  bj-snmoore  33561  bj-bary1lem1  33660  poimirlem26  33924  heicant  33933  ismblfin  33939  volsupnfl  33943  itg2addnclem2  33950  itg2addnc  33952  rngodm1dm2  34218  rngoidmlem  34222  rngo1cl  34225  rngoueqz  34226  zerdivemp1x  34233  dvheveccl  37133  rp-isfinite5  38646  clcnvlem  38713  relexpxpmin  38792  gneispace  39214