Theorem eqtr2 2794

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765

This theorem is referenced by:  eqvincg  3550  reusv3i  5152  moop2  5241  relopabi  5537  relop  5564  f0rn0  6387  fliftfun  6882  addlsub  10849  wrd2ind  13907  wrd2indOLD  13908  fsum2dlem  14975  fprodser  15153  0dvds  15480  cncongr1  15857  4sqlem12  16138  cshwshashlem1  16275  catideu  16794  pj1eu  18570  lspsneu  19607  1marepvmarrepid  20878  mdetunilem6  20920  qtopeu  22018  qtophmeo  22119  dscmet  22875  isosctrlem2  25088  ppiub  25472  axcgrtr  26394  axeuclid  26442  axcontlem2  26444  uhgr2edg  26683  usgredgreu  26693  uspgredg2vtxeu  26695  wlkon2n0  27140  spthonepeq  27231  usgr2wlkneq  27235  2pthon3v  27439  umgr2adedgspth  27444  clwwlknondisj  27629  frgr2wwlkeqm  27855  2wspmdisj  27861  ajmoi  28403  chocunii  28849  3oalem2  29211  adjmo  29380  cdjreui  29980  eqtrb  30010  probun  31280  bnj551  31622  soseq  32557  sltsolem1  32641  nolt02o  32660  btwnswapid  32939  bj-snsetex  33728  bj-bary1lem1  33975  poimirlem4  34285  exidu1  34524  rngoideu  34571  mapdpglem31  38232  frege55b  39551  frege55c  39572  cncfiooicclem1  41552  euoreqb  42660  aacllem  44209