Theorem eqtr 2749

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  sylan9eq  2784  eqvincg  3611  disjeq0  4415  uneqdifeq  4452  propeqop  5462  relresfld  6237  unixpid  6245  fvmptdf  6956  poseq  8114  soseq  8115  eqer  8684  xpider  8738  undifixp  8884  wemaplem2  9476  infeq5  9566  ficard  10494  winalim2  10625  addlsub  11570  pospo  18284  istos  18357  symg2bas  19307  dmatmul  22417  uhgr2edg  29188  clwlkclwwlkf1lem3  29985  eqtrb  32453  bnj545  34878  bnj934  34918  bnj953  34922  ordcmp  36428  bj-snmoore  37094  bj-isclm  37272  bj-bary1lem1  37292  poimirlem26  37633  heicant  37642  ismblfin  37648  volsupnfl  37652  itg2addnclem2  37659  itg2addnc  37661  rngodm1dm2  37919  rngoidmlem  37923  rngo1cl  37926  rngoueqz  37927  zerdivemp1x  37934  disjdmqsss  38787  dvheveccl  41099  rp-isfinite5  43499  clcnvlem  43605  relexpxpmin  43699  gneispace  44116  resipos  48956