Theorem eqtr2 2780

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753

This theorem is referenced by:  eqvincg  3468  reusv3i  5024  moop2  5114  relopabi  5401  relop  5428  restidsingOLD  5617  f0rn0  6251  fliftfun  6725  addlsub  10639  wrd2ind  13677  fsum2dlem  14700  fprodser  14878  0dvds  15204  cncongr1  15583  4sqlem12  15862  cshwshashlem1  16004  catideu  16537  pj1eu  18309  lspsneu  19325  1marepvmarrepid  20583  mdetunilem6  20625  qtopeu  21721  qtophmeo  21822  dscmet  22578  isosctrlem2  24748  ppiub  25128  axcgrtr  25994  axeuclid  26042  axcontlem2  26044  uhgr2edg  26299  usgredgreu  26309  uspgredg2vtxeu  26311  wlkon2n0  26772  spthonepeq  26858  usgr2wlkneq  26862  2pthon3v  27063  umgr2adedgspth  27068  clwwlknondisj  27260  clwwlknondisjOLD  27264  frgr2wwlkeqm  27485  2wspmdisj  27491  ajmoi  28023  chocunii  28469  3oalem2  28831  adjmo  29000  cdjreui  29600  probun  30790  bnj551  31119  soseq  32060  sltsolem1  32132  nolt02o  32151  btwnswapid  32430  bj-snsetex  33257  bj-bary1lem1  33472  poimirlem4  33726  exidu1  33968  rngoideu  34015  mapdpglem31  37494  frege55b  38693  frege55c  38714  cncfiooicclem1  40609  aacllem  43060