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

Theorem eqtr2 2158
 Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Assertion
Ref Expression
eqtr2 ((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)

Proof of Theorem eqtr2
StepHypRef Expression
1 eqcom 2141 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
2 eqtr 2157 . 2 ((𝐵 = 𝐴𝐴 = 𝐶) → 𝐵 = 𝐶)
31, 2sylanb 282 1 ((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132 This theorem is referenced by:  eqvinc  2808  eqvincg  2809  moop2  4173  reusv3i  4380  relop  4689  f0rn0  5317  fliftfun  5697  th3qlem1  6531  enq0ref  7248  enq0tr  7249  genpdisj  7338  addlsub  8139  fsum2dlemstep  11210  0dvds  11519  cncongr1  11790
 Copyright terms: Public domain W3C validator