Theorem eqtr2 2837

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 2824	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2		eqtr 2836	. 2 ⊢ ((𝐵 = 𝐴 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
3	1, 2	sylanb 572	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2810

This theorem is referenced by:  eqvincg  3534  reusv3i  5084  moop2  5166  relopabi  5458  relop  5485  f0rn0  6312  fliftfun  6793  addlsub  10739  wrd2ind  13708  fsum2dlem  14731  fprodser  14907  0dvds  15232  cncongr1  15606  4sqlem12  15884  cshwshashlem1  16021  catideu  16547  pj1eu  18317  lspsneu  19337  1marepvmarrepid  20600  mdetunilem6  20642  qtopeu  21741  qtophmeo  21842  dscmet  22598  isosctrlem2  24773  ppiub  25153  axcgrtr  26019  axeuclid  26067  axcontlem2  26069  uhgr2edg  26325  usgredgreu  26335  uspgredg2vtxeu  26337  wlkon2n0  26800  spthonepeq  26886  usgr2wlkneq  26890  2pthon3v  27093  umgr2adedgspth  27098  clwwlknondisj  27290  clwwlknondisjOLD  27295  frgr2wwlkeqm  27516  2wspmdisj  27522  ajmoi  28052  chocunii  28498  3oalem2  28860  adjmo  29029  cdjreui  29629  probun  30816  bnj551  31144  soseq  32084  sltsolem1  32156  nolt02o  32175  btwnswapid  32454  bj-snsetex  33267  bj-bary1lem1  33484  poimirlem4  33732  exidu1  33972  rngoideu  34019  mapdpglem31  37489  frege55b  38696  frege55c  38717  cncfiooicclem1  40591  aacllem  43123