Theorem eqtr 1529

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

Assertion

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

Proof of Theorem eqtr

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

Syntax hints:   -> wi 3   /\ wa 221   = wceq 988

This theorem is referenced by:  eqtr2 1530  eqtr3 1531  preqsn 2534  ider 4353  eqer 4355  xpmapenlem4 4588  infeq5 4707  cfom 5005  uzindOLD 6321  sn0top 7769  cnconst 7900  ring2 8268  efif1lem5 8853  neiopne 10591  oooeqim2 10593  domfldref 10598  twpar2 10604  homcard 10675  subspemp 10692  cnfilca 10715  usinuniop 10753  imonclem 10876  isepic 10887

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-17 1003  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1505

Copyright terms: Public domain