Theorem eqtrt 1495

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 1484	. 2 |- (A = B -> (A = C <-> B = C))
2	1	biimpar 419	1 |- ((A = B /\ B = C) -> A = C)

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

This theorem is referenced by:  eqtr2t 1496  eqtr3t 1497  preqsn 2490  ider 4275  eqer 4277  xpmapenlem4 4505  infeq5 4630  cfom 4928  uzindOLD 6210  sn0top 7644  cnconst 7777  ring2 8145  efif1lem5 8729  neiopne 10463  oooeqim2 10465  homcard 10525  cnfilca 10562  imonclem 10712

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