Theorem eqtr 2790

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2762

This theorem is referenced by:  sylan9eq  2825  eqvincg  3615  disjeq0  4422  uneqdifeq  4458  propeqop  5494  relresfld  6281  unixpid  6289  fvmptdf  7000  poseq  8157  soseq  8158  eqer  8734  xpider  8789  undifixp  8935  wemaplem2  9512  infeq5  9609  ficard  10552  winalim2  10684  addlsub  11633  pospo  18402  istos  18475  symg2bas  19466  dmatmul  22637  uhgr2edg  29528  clwlkclwwlkf1lem3  30327  eqtrb  32790  bnj545  35253  bnj934  35293  bnj953  35297  ordcmp  36906  bj-snmoore  37703  bj-isclm  37883  bj-bary1lem1  37903  wl-dfcleq  38108  poimirlem26  38245  heicant  38254  ismblfin  38260  volsupnfl  38264  itg2addnclem2  38271  itg2addnc  38273  rngodm1dm2  38531  rngoidmlem  38535  rngo1cl  38538  rngoueqz  38539  zerdivemp1x  38546  disjdmqsss  39504  dvheveccl  41836  rp-isfinite5  44195  clcnvlem  44301  relexpxpmin  44395  gneispace  44812  resipos  49702