Theorem eqtr3 1907

Description: A transitive law for class equality.

Assertion

Ref	Expression
eqtr3	|- ((A = C /\ B = C) -> A = B)

Proof of Theorem eqtr3

Step	Hyp	Ref	Expression
1		eqtr 1904	. 2 |- ((A = C /\ C = B) -> A = B)
2		eqcom 1886	. 2 |- (B = C <-> C = B)
3	1, 2	sylan2b 501	1 |- ((A = C /\ B = C) -> A = B)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298

This theorem is referenced by:  eueq 2427  euind 2439  reuind 2450  preqsn 3157  reuunisn 3822  eualeq 3823  eualeqhb 3824  euexeqOLD 3826  eufromeq1 3828  eufromeq5 3832  euobj1 3834  xpcan 4348  xpcan2 4350  funopg 4454  funsnOLD 4464  foco 4628  oawordeulem 5236  negeui 6510  xrlttri 6727  receui 6890  grpinveu 9348  ringsn 9490  psrn 9993  exidu1 10373  5oalem4 11237  bra11 11679  bnj149 13241  bnj594 13300  bnj953 13343  fz1eqblem 13608  mulgcdlem2 13757  mpt2fun 13843  wfr3g 13956  frr3g 13980  axsltsolem1 14006  axbday 14012  nocvxminlem 14028  axfelem15 14045  surrc2 14390  restidsing 14391  topgrpi 14972  dualcat2 15133  imonclem 15162  ismonc 15163  prfunOLD 15677  heiborlem18 15972  phtpyco 16056  pcoloopf 16079  pi1f 16093  pi1val 16094  pi1gp 16095  prtlem11 16268  prter2 16285  grpinveuNEW 17123

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain