Theorem eqtr 2758

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  eqtr2OLD  2760  eqtr3OLD  2762  sylan9eq  2795  eqvincg  3648  disjeq0  4462  uneqdifeq  4499  propeqop  5517  relresfld  6298  unixpid  6306  fvmptdf  7022  poseq  8182  soseq  8183  eqer  8780  xpider  8827  undifixp  8973  wemaplem2  9585  infeq5  9675  ficard  10603  winalim2  10734  addlsub  11677  pospo  18403  istos  18476  symg2bas  19425  dmatmul  22519  uhgr2edg  29240  clwlkclwwlkf1lem3  30035  eqtrb  32502  bnj545  34888  bnj934  34928  bnj953  34932  ordcmp  36430  bj-snmoore  37096  bj-isclm  37274  bj-bary1lem1  37294  poimirlem26  37633  heicant  37642  ismblfin  37648  volsupnfl  37652  itg2addnclem2  37659  itg2addnc  37661  rngodm1dm2  37919  rngoidmlem  37923  rngo1cl  37926  rngoueqz  37927  zerdivemp1x  37934  disjdmqsss  38784  dvheveccl  41095  rp-isfinite5  43507  clcnvlem  43613  relexpxpmin  43707  gneispace  44124