Theorem eqtr 2779

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753

This theorem is referenced by:  eqtr2  2780  eqtr3  2781  sylan9eq  2814  eqvincg  3468  disjeq0  4166  uneqdifeq  4201  uneqdifeqOLD  4202  preqsnOLDOLD  4542  propeqop  5118  relresfld  5823  unixpid  5831  eqer  7948  xpider  7987  undifixp  8112  wemaplem2  8619  infeq5  8709  ficard  9599  winalim2  9730  addlsub  10659  pospo  17194  istos  17256  symg2bas  18038  dmatmul  20525  uhgr2edg  26320  clwlkclwwlkf1lem3  27150  bnj545  31293  bnj934  31333  bnj953  31337  poseq  32080  soseq  32081  ordcmp  32773  bj-snmoore  33392  bj-bary1lem1  33490  poimirlem26  33766  heicant  33775  ismblfin  33781  volsupnfl  33785  itg2addnclem2  33793  itg2addnc  33795  rngodm1dm2  34062  rngoidmlem  34066  rngo1cl  34069  rngoueqz  34070  zerdivemp1x  34077  dvheveccl  36921  rp-isfinite5  38383  clcnvlem  38450  relexpxpmin  38529  gneispace  38952