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

Theorem eqtr2 2136
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 2119 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
2 eqtr 2135 . 2 ((𝐵 = 𝐴𝐴 = 𝐶) → 𝐵 = 𝐶)
31, 2sylanb 282 1 ((𝐴 = 𝐵𝐴 = 𝐶) → 𝐵 = 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqvinc  2782  eqvincg  2783  moop2  4143  reusv3i  4350  relop  4659  f0rn0  5287  fliftfun  5665  th3qlem1  6499  enq0ref  7209  enq0tr  7210  genpdisj  7299  addlsub  8100  fsum2dlemstep  11171  0dvds  11440  cncongr1  11711
  Copyright terms: Public domain W3C validator