Theorem eqtr 2754

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  eqtr2OLD  2756  eqtr3OLD  2758  sylan9eq  2791  eqvincg  3601  disjeq0  4420  uneqdifeq  4455  propeqop  5469  relresfld  6233  unixpid  6241  fvmptdf  6959  poseq  8095  soseq  8096  eqer  8690  xpider  8734  undifixp  8879  wemaplem2  9492  infeq5  9582  ficard  10510  winalim2  10641  addlsub  11580  pospo  18248  istos  18321  symg2bas  19188  dmatmul  21883  uhgr2edg  28219  clwlkclwwlkf1lem3  29013  eqtrb  31466  bnj545  33596  bnj934  33636  bnj953  33640  ordcmp  34995  bj-snmoore  35657  bj-isclm  35835  bj-bary1lem1  35855  poimirlem26  36177  heicant  36186  ismblfin  36192  volsupnfl  36196  itg2addnclem2  36203  itg2addnc  36205  rngodm1dm2  36464  rngoidmlem  36468  rngo1cl  36471  rngoueqz  36472  zerdivemp1x  36479  disjdmqsss  37337  dvheveccl  39648  rp-isfinite5  41911  clcnvlem  42017  relexpxpmin  42111  gneispace  42528