In [1], the principle of semisubstitutivity of implication (SSI) was introduced for ordinary PC and quantification theory. This metatheorem generalizes the notions of “antecedent” and “consequent” to cover all wf subformulas of a given formula; each such subformula will be classified as being either in “antecedental position” (A-pos) or “consequential position” (C-pos). It is simplest to check these positions in a conjunction-negation primitive system: reduce a formula φ to primitive notation (K—N) ; choose a subformula ψ of φ; count the negation signs in φ within whose scope ψ falls.