Theorem eqtr2 2762

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqvincg  3570  reusv3i  5322  moop2  5410  relopabi  5721  relop  5748  f0rn0  6643  fliftfun  7163  addlsub  11321  wrd2ind  14364  fsum2dlem  15410  fprodser  15587  0dvds  15914  cncongr1  16300  4sqlem12  16585  cshwshashlem1  16725  catideu  17301  pj1eu  19217  lspsneu  20300  1marepvmarrepid  21632  mdetunilem6  21674  qtopeu  22775  qtophmeo  22876  dscmet  23634  isosctrlem2  25874  ppiub  26257  axcgrtr  27186  axeuclid  27234  axcontlem2  27236  uhgr2edg  27478  usgredgreu  27488  uspgredg2vtxeu  27490  wlkon2n0  27936  spthonepeq  28021  usgr2wlkneq  28025  2pthon3v  28209  umgr2adedgspth  28214  clwwlknondisj  28376  frgr2wwlkeqm  28596  2wspmdisj  28602  ajmoi  29121  chocunii  29564  3oalem2  29926  adjmo  30095  cdjreui  30695  eqtrb  30724  probun  32286  bnj551  32622  satfv0fun  33233  satffunlem  33263  satffunlem1lem1  33264  satffunlem2lem1  33266  soseq  33730  sltsolem1  33805  nolt02o  33825  nogt01o  33826  btwnswapid  34246  bj-snsetex  35080  bj-bary1lem1  35409  poimirlem4  35708  exidu1  35941  rngoideu  35988  mapdpglem31  39644  remul01  40311  frege55b  41394  frege55c  41415  cncfiooicclem1  43324  euoreqb  44488  aacllem  46391