Theorem eqtr3t 1491

Description: A transitive law for class equality.

Assertion

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

Proof of Theorem eqtr3t

Step	Hyp	Ref	Expression
1		eqtrt 1489	. 2 |- ((A = C /\ C = B) -> A = B)
2		eqcom 1474	. 2 |- (B = C <-> C = B)
3	1, 2	sylan2b 452	1 |- ((A = C /\ B = C) -> A = B)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 954

This theorem is referenced by:  eueq 1912  preqsn 2482  reuunisn 2890  funsn 3535  funopg 3539  foco 3673  oawordeulem 4178  negeu 5335  xrlttrit 5533  receu 5678  grpinveu 8014  ringsn 8115  5oalem4 9542  bra11 9979  imonclem 10619  ismonc 10620

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain