Theorem eqtr2 2671

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644

This theorem is referenced by:  eqvincg  3360  reusv3i  4905  moop2  4995  relopabi  5278  relop  5305  restidsingOLD  5494  f0rn0  6128  fliftfun  6602  addlsub  10485  wrd2ind  13523  fsum2dlem  14545  fprodser  14723  0dvds  15049  cncongr1  15428  4sqlem12  15707  cshwshashlem1  15849  catideu  16383  pj1eu  18155  lspsneu  19171  1marepvmarrepid  20429  mdetunilem6  20471  qtopeu  21567  qtophmeo  21668  dscmet  22424  isosctrlem2  24594  ppiub  24974  axcgrtr  25840  axeuclid  25888  axcontlem2  25890  uhgr2edg  26145  usgredgreu  26155  uspgredg2vtxeu  26157  wlkon2n0  26618  spthonepeq  26704  usgr2wlkneq  26708  2pthon3v  26908  umgr2adedgspth  26913  clwwlknondisj  27086  clwwlknondisjOLD  27090  frgr2wwlkeqm  27311  2wspmdisj  27317  ajmoi  27842  chocunii  28288  3oalem2  28650  adjmo  28819  cdjreui  29419  probun  30609  bnj551  30938  soseq  31879  sltsolem1  31951  nolt02o  31970  btwnswapid  32249  bj-snsetex  33076  bj-bary1lem1  33291  poimirlem4  33543  exidu1  33785  rngoideu  33832  mapdpglem31  37309  frege55b  38508  frege55c  38529  cncfiooicclem1  40424  aacllem  42875