Theorem eqtr 2760

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 2741	. 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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqtr2OLD  2762  eqtr3OLD  2764  sylan9eq  2797  eqvincg  3648  disjeq0  4456  uneqdifeq  4493  propeqop  5512  relresfld  6296  unixpid  6304  fvmptdf  7022  poseq  8183  soseq  8184  eqer  8781  xpider  8828  undifixp  8974  wemaplem2  9587  infeq5  9677  ficard  10605  winalim2  10736  addlsub  11679  pospo  18390  istos  18463  symg2bas  19410  dmatmul  22503  uhgr2edg  29225  clwlkclwwlkf1lem3  30025  eqtrb  32493  bnj545  34909  bnj934  34949  bnj953  34953  ordcmp  36448  bj-snmoore  37114  bj-isclm  37292  bj-bary1lem1  37312  poimirlem26  37653  heicant  37662  ismblfin  37668  volsupnfl  37672  itg2addnclem2  37679  itg2addnc  37681  rngodm1dm2  37939  rngoidmlem  37943  rngo1cl  37946  rngoueqz  37947  zerdivemp1x  37954  disjdmqsss  38803  dvheveccl  41114  rp-isfinite5  43530  clcnvlem  43636  relexpxpmin  43730  gneispace  44147