The "introduction to constructive logic" on the landing page says that Line 6 is "modus tollendo ponens". But the Wikipedia page on modus tollendo ponens says that from $\neg(A\wedge B)$ and $A$ it infers $\neg B$, whereas it seems to me that what's going on in this example is from $C \vee D$ and $\neg D$ we infer $C$, which is the disjunctive syllogism instead.
The "introduction to constructive logic" on the landing page says that Line 6 is "modus tollendo ponens". But the Wikipedia page on modus tollendo ponens says that from$\neg(A\wedge B)$ and $A$ it infers $\neg B$ , whereas it seems to me that what's going on in this example is from $C \vee D$ and $\neg D$ we infer $C$ , which is the disjunctive syllogism instead.