 As is standard for an axiomatic formulation of logic, a derivation of a formula of sentential logic in PM will consist of an instance of one of the six axioms, the result of a substitution in a preceding line, or the application of modus ponens to two preceding lines. Theorems of PM will be proved in order, allowing the use of (instances of) preceding theorems as lines in later derivations.