HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 eqeq1 1518 . 2 |- (A = B -> (A = C <-> B = C))
21biimpar 417 1 |- ((A = B /\ B = C) -> A = C)
Colors of variables: wff set class
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