Theorem eqtr2 2757

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  eqvincg  3545  reusv3i  5282  moop2  5370  relopabi  5677  relop  5704  f0rn0  6582  fliftfun  7099  addlsub  11213  wrd2ind  14253  fsum2dlem  15297  fprodser  15474  0dvds  15801  cncongr1  16187  4sqlem12  16472  cshwshashlem1  16612  catideu  17132  pj1eu  19040  lspsneu  20114  1marepvmarrepid  21426  mdetunilem6  21468  qtopeu  22567  qtophmeo  22668  dscmet  23424  isosctrlem2  25656  ppiub  26039  axcgrtr  26960  axeuclid  27008  axcontlem2  27010  uhgr2edg  27250  usgredgreu  27260  uspgredg2vtxeu  27262  wlkon2n0  27708  spthonepeq  27793  usgr2wlkneq  27797  2pthon3v  27981  umgr2adedgspth  27986  clwwlknondisj  28148  frgr2wwlkeqm  28368  2wspmdisj  28374  ajmoi  28893  chocunii  29336  3oalem2  29698  adjmo  29867  cdjreui  30467  eqtrb  30496  probun  32052  bnj551  32388  satfv0fun  33000  satffunlem  33030  satffunlem1lem1  33031  satffunlem2lem1  33033  soseq  33483  sltsolem1  33564  nolt02o  33584  nogt01o  33585  btwnswapid  34005  bj-snsetex  34839  bj-bary1lem1  35165  poimirlem4  35467  exidu1  35700  rngoideu  35747  mapdpglem31  39403  remul01  40039  frege55b  41123  frege55c  41144  cncfiooicclem1  43052  euoreqb  44216  aacllem  46119