Theorem eqtr 2755

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 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

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

This theorem is referenced by:  sylan9eq  2790  eqvincg  3601  disjeq0  4407  uneqdifeq  4444  propeqop  5454  relresfld  6233  unixpid  6241  fvmptdf  6947  poseq  8100  soseq  8101  eqer  8672  xpider  8727  undifixp  8874  wemaplem2  9454  infeq5  9548  ficard  10477  winalim2  10609  addlsub  11555  pospo  18268  istos  18341  symg2bas  19324  dmatmul  22443  uhgr2edg  29262  clwlkclwwlkf1lem3  30062  eqtrb  32528  bnj545  35030  bnj934  35070  bnj953  35074  ordcmp  36620  bj-snmoore  37287  bj-isclm  37465  bj-bary1lem1  37485  poimirlem26  37816  heicant  37825  ismblfin  37831  volsupnfl  37835  itg2addnclem2  37842  itg2addnc  37844  rngodm1dm2  38102  rngoidmlem  38106  rngo1cl  38109  rngoueqz  38110  zerdivemp1x  38117  disjdmqsss  39075  dvheveccl  41407  rp-isfinite5  43795  clcnvlem  43901  relexpxpmin  43995  gneispace  44412  resipos  49257