Negation with De Morgan’s law I'm having a hard time getting my head around transformation proofs. There is one particular example demonstration in the material I'm studying which I can't make sense of 
From this 
¬ (¬ (¬ p) ∨ ¬ (¬ q)) 
We get 
¬ (¬ (¬ p ∧ ¬ q))  
I can see that we've gone from a disjunction to a conjunction, but I don't get why the negation that was outside of q was removed. 
De Morgan’s first law
(p ∧ q) ≡ ¬ p ∨ ¬ q
 A: Let's define some abbreviations:
$$\begin{align}
A &= \neg p \\
B &= \neg q \\
C &= (\neg A) \lor (\neg B) \\
D &= \neg(A\land B) \end{align}$$
Then you're asking about rewriting $\neg C$ to $\neg D$ (unfold all the abbreviations if you're unsure that this is actually what you're doing).
But $C$ and $D$ are clearly equivalent by De Morgan's laws, and since $\neg C$ and $\neg D$ is just $C$ and $D$ both placed in the same context, they will be equivalent too.
A: $$\neg(\neg(\neg p) \vee \neg(\neg q))=\neg(p\vee q)=\neg p\wedge \neg q=\neg(\neg(\neg p \wedge\neg q)))$$
A: First note that the first $\neg$ is useless to prove the "equality". You can write your problem as follows: $$\neg \neg p \lor \neg \neg q$$ which you can reduce to $p\lor q$. Second you apply the de Morgan's law (the correct one was given by Mr. Newman) and the result appears.
A: The steps to get from the first formula to the second one are as follows:


*

*$\neg( p \vee q)\quad\quad\quad$ (because $\neg(\neg x) \equiv x$, double negation)

*$\neg p \land \neg q\quad\quad\quad$ (because $\neg(x \vee y) \equiv \neg x \land \neg y$, De Morgan)

*$\neg(\neg(\neg p \land \neg q))\quad$ (because $\neg(\neg x) \equiv x$, double negation)

A: One approach to help see what is going on is to use a proof checker to make sure one is using well-formed formulas and to guarantee that the rules are being followed.  It will also tell you if you have succeeded in proving a goal.  
I entered the string, "~(~(~P)v~(~Q))" into the proof checker to get this well-formed formula acceptable to the proof checker with extra parentheses removed: "¬(¬¬P ∨ ¬¬Q)"
Here is the proof:

I set the goal to derive $\neg P \land \neg Q$. Since I am required to follow the inference rules I cannot jump and mentally perform a double negative elimination (DNE). I have to derive a line on which I can use that inference rule first.
Here is the question:

I can see that we've gone from a disjunction to a conjunction, but I don't get why the negation that was outside of q was removed.

When the parentheses around $\neg(\neg Q)$ are removed we get $\neg \neg Q$. This was done automatically by the proof checker. Using De Morgan's law on line 2 added another negation to $Q$. Once I was able to derive $\neg \neg \neg Q$ on line 4, I was able to use double negation elimination (DNE) to derive $\neg Q$ on line 6.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
