Theorem eqtr2t 1496

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 1495	. 2 |- ((B = A /\ A = C) -> B = C)
2		eqcom 1480	. 2 |- (A = B <-> B = A)
3	1, 2	sylanb 451	1 |- ((A = B /\ A = C) -> B = C)

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

This theorem is referenced by:  csbie2t 2036  moop2 2807  relop 3281  th3qlem1 4320  aceq5lem4 4748  creur 6743  creui 6744  replimt 6762  ajmoi 8515  chocuni 9167  3oalem2 9603  adjmo 9753  adjvalvalt 9856  cdjreu 10354

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain