Theorem eqtr3t 1493

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 1491	. 2 |- ((A = C /\ C = B) -> A = B)
2		eqcom 1476	. 2 |- (B = C <-> C = B)
3	1, 2	sylan2b 452	1 |- ((A = C /\ B = C) -> A = B)

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

This theorem is referenced by:  eueq 1914  preqsn 2484  reuunisn 2892  funsn 3540  funopg 3544  foco 3679  oawordeulem 4185  negeu 5342  xrlttrit 5539  receu 5684  grpinveu 8047  ringsn 8148  psrn 8633  5oalem4 9593  bra11 10032  imonclem 10690  ismonc 10691

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974  ax-ext 1459

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

Copyright terms: Public domain