Theorem eqtr2 2842

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

Assertion

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

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqcom 2828	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2		eqtr 2841	. 2 ⊢ ((𝐵 = 𝐴 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
3	1, 2	sylanb 583	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  eqvincg  3640  reusv3i  5296  moop2  5384  relopabi  5688  relop  5715  f0rn0  6558  fliftfun  7059  addlsub  11050  wrd2ind  14079  fsum2dlem  15119  fprodser  15297  0dvds  15624  cncongr1  16005  4sqlem12  16286  cshwshashlem1  16423  catideu  16940  pj1eu  18816  lspsneu  19889  1marepvmarrepid  21178  mdetunilem6  21220  qtopeu  22318  qtophmeo  22419  dscmet  23176  isosctrlem2  25391  ppiub  25774  axcgrtr  26695  axeuclid  26743  axcontlem2  26745  uhgr2edg  26984  usgredgreu  26994  uspgredg2vtxeu  26996  wlkon2n0  27442  spthonepeq  27527  usgr2wlkneq  27531  2pthon3v  27716  umgr2adedgspth  27721  clwwlknondisj  27884  frgr2wwlkeqm  28104  2wspmdisj  28110  ajmoi  28629  chocunii  29072  3oalem2  29434  adjmo  29603  cdjreui  30203  eqtrb  30232  probun  31672  bnj551  32008  satfv0fun  32613  satffunlem  32643  satffunlem1lem1  32644  satffunlem2lem1  32646  soseq  33091  sltsolem1  33175  nolt02o  33194  btwnswapid  33473  bj-snsetex  34270  bj-bary1lem1  34586  poimirlem4  34890  exidu1  35128  rngoideu  35175  mapdpglem31  38833  remul01  39230  frege55b  40236  frege55c  40257  cncfiooicclem1  42169  euoreqb  43302  aacllem  44896