 Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqtr GIF version

Theorem eqtr 2105
 Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
Assertion
Ref Expression
eqtr ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)

Proof of Theorem eqtr
StepHypRef Expression
1 eqeq1 2094 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
21biimpar 291 1 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   = wceq 1289 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070 This theorem depends on definitions:  df-bi 115  df-cleq 2081 This theorem is referenced by:  eqtr2  2106  eqtr3  2107  sylan9eq  2140  eqvinc  2740  eqvincg  2741  uneqdifeqim  3368  preqsn  3619  dtruex  4375  relresfld  4960  relcoi1  4962  eqer  6324  xpiderm  6363  addlsub  7848  bj-findis  11874
 Copyright terms: Public domain W3C validator