Theorem eqtr2 2764

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)

Assertion

Ref	Expression
eqtr2	⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqeq1 2744	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpa 476	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqvincg  3661  reusv3i  5422  moop2  5521  relopabi  5846  relop  5875  f0rn0  6806  fliftfun  7348  soseq  8200  addlsub  11706  wrd2ind  14771  fsum2dlem  15818  fprodser  15997  0dvds  16325  cncongr1  16714  4sqlem12  17003  cshwshashlem1  17143  catideu  17733  pj1eu  19738  lspsneu  21148  1marepvmarrepid  22602  mdetunilem6  22644  qtopeu  23745  qtophmeo  23846  dscmet  24606  isosctrlem2  26880  ppiub  27266  sltsolem1  27738  nolt02o  27758  nogt01o  27759  axcgrtr  28948  axeuclid  28996  axcontlem2  28998  uhgr2edg  29243  usgredgreu  29253  uspgredg2vtxeu  29255  wlkon2n0  29702  spthonepeq  29788  usgr2wlkneq  29792  2pthon3v  29976  umgr2adedgspth  29981  clwwlknondisj  30143  frgr2wwlkeqm  30363  2wspmdisj  30369  ajmoi  30890  chocunii  31333  3oalem2  31695  adjmo  31864  cdjreui  32464  eqtrb  32502  probun  34384  bnj551  34718  satfv0fun  35339  satffunlem  35369  satffunlem1lem1  35370  satffunlem2lem1  35372  r1peuqusdeg1  35611  btwnswapid  35981  bj-snsetex  36929  bj-bary1lem1  37277  poimirlem4  37584  exidu1  37816  rngoideu  37863  mapdpglem31  41660  grpods  42151  remul01  42383  frege55b  43859  frege55c  43880  cncfiooicclem1  45814  euoreqb  47024  isuspgrim0lem  47755  aacllem  48895