Theorem eqtr2t 1493

Description: A transitive law for class equality.

Assertion

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

Proof of Theorem eqtr2t

Step	Hyp	Ref	Expression
1		eqtrt 1492	. 2 |- ((B = A /\ A = C) -> B = C)
2		eqcom 1477	. 2 |- (A = B <-> B = A)
3	1, 2	sylanb 449	1 |- ((A = B /\ A = C) -> B = C)

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

This theorem is referenced by:  csbie2t 2033  moop2 2801  relop 3275  th3qlem1 4314  aceq5lem4 4738  creur 6742  creui 6743  replimt 6761  ajmoi 8519  chocuni 9172  3oalem2 9608  adjmo 9758  adjvalvalt 9861  cdjreu 10359

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain