Page:Russell, Whitehead - Principia Mathematica, vol. I, 1910.djvu/161

In the second line of the above proof, "$\scriptstyle {\sim \phi y\lor \phi y}$" is taken as the value for the argument $\scriptstyle {y}$, of the function "$\scriptstyle {\sim \phi x\lor \phi y}$," where $\scriptstyle {x}$ is the argument. A similar method of using *9.1 is employed in most of the following proofs.

*1.11 is used, as in the third line of the above proof, in almost all steps except such as are mere applications of definitions. Hence it will not be further referred to, unless in cases where its employment is obscure or specially important.

*9.21. $\scriptstyle {\sim :.(x).\phi x\supset \psi x.\supset :(x).\phi x.\supset .(x).\psi x}$

I.e. if $\scriptstyle {\phi x}$ always implies $\scriptstyle {\psi x}$, then "$\scriptstyle {\phi x}$ always" implies "$\scriptstyle {\psi x}$ always." The use of this proposition is constant throughout the remainder of this work.

Dem.${\begin{array}{rcl}\scriptstyle {\sim .*2.08.}&\scriptstyle {\supset \vdash :\phi z\supset \psi z.\supset .\phi z\supset \psi z}&\scriptstyle {\text{(1)}}\\\end{array}}$