Theorem eqtrt 1490

Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13.

Assertion

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

Proof of Theorem eqtrt

Step	Hyp	Ref	Expression
1		eqeq1 1479	. 2 |- (A = B -> (A = C <-> B = C))
2	1	biimpar 417	1 |- ((A = B /\ B = C) -> A = C)

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

This theorem is referenced by:  eqtr2t 1491  eqtr3t 1492  preqsn 2483  ider 4262  eqer 4264  xpmapenlem4 4488  infeq5 4604  cfom 4899  uzindOLD 6166  sn0top 7607  cnconst 7740  ring2 8113  efif1lem5 8684  neiopne 10427  oooeqim2 10429  homcard 10485  cnfilca 10510  imonclem 10655

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 1458

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

Copyright terms: Public domain