Theorem eqtr2 2642

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	|- ( ( A = B /\ A = C ) -> B = C )

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqcom 2629	. 2 |- ( A = B <-> B = A )
2		eqtr 2641	. 2 |- ( ( B = A /\ A = C ) -> B = C )
3	1, 2	sylanb 489	1 |- ( ( A = B /\ A = C ) -> B = C )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqvincg  3329  reusv3i  4875  moop2  4966  relopabi  5245  relop  5272  restidsingOLD  5459  f0rn0  6090  fliftfun  6562  addlsub  10447  wrd2ind  13477  fsum2dlem  14501  fprodser  14679  0dvds  15002  cncongr1  15381  4sqlem12  15660  cshwshashlem1  15802  catideu  16336  pj1eu  18109  lspsneu  19123  1marepvmarrepid  20381  mdetunilem6  20423  qtopeu  21519  qtophmeo  21620  dscmet  22377  isosctrlem2  24549  ppiub  24929  axcgrtr  25795  axeuclid  25843  axcontlem2  25845  uhgr2edg  26100  usgredgreu  26110  uspgredg2vtxeu  26112  wlkon2n0  26562  spthonepeq  26648  usgr2wlkneq  26652  2pthon3v  26839  umgr2adedgspth  26844  clwwlksndisj  26973  frgr2wwlkeqm  27195  2wspmdisj  27201  ajmoi  27714  chocunii  28160  3oalem2  28522  adjmo  28691  cdjreui  29291  probun  30481  bnj551  30812  soseq  31751  sltsolem1  31826  nolt02o  31845  btwnswapid  32124  bj-snsetex  32951  bj-bary1lem1  33161  poimirlem4  33413  exidu1  33655  rngoideu  33702  mapdpglem31  36992  frege55b  38191  frege55c  38212  cncfiooicclem1  40106  aacllem  42547