These are the formal principles of deduction employed in Principia Mathematica. A formal principle of deduction has a double use, and it is in order to make this clear that we have cited the above five propositions. It has a use as the premiss of an inference, and a use as establishing the fact that the premiss implies the conclusion. In the schema of an inference we have a proposition , and a proposition " implies ," from which we infer . Now when we are concerned with the principles of deduction, our apparatus of primitive propositions has to yield both the and the " implies " of our inferences. That is to say, our rules of deduction are to be used, not only as rules, which is their use for establishing " implies " but also as substantive premisses, i.e. as the of our schema. Suppose, for example, we wish to prove that if implies , then if implies it follows that implies . We have here a relation of three propositions which state implications. Put implies , implies , and implies . Then we have to prove that implies that implies . Now take the fifth of our above principles, substitute not- for , and remember that "not- or " is by definition the same as " implies ." Thus our fifth principle yields: "If implies , then ' implies ' implies 'implies ,'" i.e. "implies that implies ." Call this proposition . But the fourth of our principles, when we substitute not-, not-, for and , and remember the definition of implication, becomes: "If implies that implies , then implies that implies ." Writing in place of , in place of , and in place of , this becomes: "If implies that implies , then implies that implies ." Call this . [Pg 150] Now we proved by means of our fifth principle that " implies that implies ," which was what we called . Thus we have here an instance of the schema of inference, since represents the of our scheme, and represents the " implies ." Hence we arrive at , namely, " implies that implies ," which was the proposition to be proved. In this proof, the adaptation of our fifth principle, which yields , occurs as a substantive premiss; while the adaptation of our fourth principle, which yields , is used to give the form of the inference. The formal and material employments of premisses in the theory of deduction are closely intertwined, and it is not very important to keep them separated, provided we realise that they are in theory distinct.