Theorem eqtr 2641

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqtr2  2642  eqtr3  2643  sylan9eq  2676  eqvincg  3329  uneqdifeq  4057  uneqdifeqOLD  4058  preqsnOLD  4394  propeqop  4970  relresfld  5662  unixpid  5670  eqer  7777  eqerOLD  7778  xpider  7818  undifixp  7944  wemaplem2  8452  infeq5  8534  ficard  9387  winalim2  9518  addlsub  10447  pospo  16973  istos  17035  symg2bas  17818  dmatmul  20303  uhgr2edg  26100  bnj545  30965  bnj934  31005  bnj953  31009  poseq  31750  soseq  31751  ordcmp  32446  bj-snmoore  33068  bj-bary1lem1  33161  poimirlem26  33435  heicant  33444  ismblfin  33450  volsupnfl  33454  itg2addnclem2  33462  itg2addnc  33464  rngodm1dm2  33731  rngoidmlem  33735  rngo1cl  33738  rngoueqz  33739  zerdivemp1x  33746  dvheveccl  36401  rp-isfinite5  37863  clcnvlem  37930  relexpxpmin  38009  gneispace  38432