I wanted to read Whitehead and Russells Principia Mathematica. I think that I am beginning to get the hang of the notation but I seen to be stuck on the proof of *2.01. They prove that $\vdash : p \supset \sim p \cdot \supset \cdot \sim p $. I understand line 1 of the proof but I cant see the reason for the second line. I will try to reporduce the proof here. \begin{align*} \left[ \text{Taut} \frac{\sim p}{p} \right] &\vdash:\sim p \vee \sim p . \supset . \sim p \\ \left[ \text{(1).(*1.01)}\right ] &\vdash: p \supset \sim p . \supset . \sim p \end{align*}
From my understanding, the bracket represents the references that justifies the assertion. However, *1.01 is just the definition of implication $\sim p \vee q$. How did they go from $(\sim p \lor \sim p)$ to $(p \supset \sim p)$? Wouldn't that require double negation which hasn't been proven yet?