Theorem eqtr2 2758

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 2741	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpa 476	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 2709

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

This theorem is referenced by:  eqvincg  3591  reusv3i  5341  moop2  5450  relopabi  5771  relop  5799  f0rn0  6719  fliftfun  7260  soseq  8102  addlsub  11557  wrd2ind  14676  fsum2dlem  15723  fprodser  15905  0dvds  16236  cncongr1  16627  4sqlem12  16918  cshwshashlem1  17057  catideu  17632  pj1eu  19662  lspsneu  21113  1marepvmarrepid  22550  mdetunilem6  22592  qtopeu  23691  qtophmeo  23792  dscmet  24547  isosctrlem2  26796  ppiub  27181  ltssolem1  27653  nolt02o  27673  nogt01o  27674  axcgrtr  28998  axeuclid  29046  axcontlem2  29048  uhgr2edg  29291  usgredgreu  29301  uspgredg2vtxeu  29303  wlkon2n0  29748  spthonepeq  29835  usgr2wlkneq  29839  2pthon3v  30026  umgr2adedgspth  30031  clwwlknondisj  30196  frgr2wwlkeqm  30416  2wspmdisj  30422  ajmoi  30944  chocunii  31387  3oalem2  31749  adjmo  31918  cdjreui  32518  eqtrb  32558  probun  34579  bnj551  34901  fineqvnttrclselem1  35281  satfv0fun  35569  satffunlem  35599  satffunlem1lem1  35600  satffunlem2lem1  35602  r1peuqusdeg1  35841  btwnswapid  36215  bj-snsetex  37286  bj-bary1lem1  37641  poimirlem4  37959  exidu1  38191  rngoideu  38238  disjimrmoeqec  39143  mapdpglem31  42163  grpods  42647  remul01  42853  frege55b  44342  frege55c  44363  cncfiooicclem1  46339  euoreqb  47569  isuspgrim0lem  48381  aacllem  50288