The law for negation as a premise tells us two things about entailment. It tells us first that a conclusion is valid if and only if the denial of that conclusion can be reduced to absurdity given the premises. This is the principle of indirect proof; it is closely tied to the entailment ¬ ¬ φ ⊨ φ (and is subject to the same concerns as is that entailment). We have no need for this principle except in the case of unanalyzed components, which we will begin to call atomic sentences. And, for reasons noted later, we need to limit the use of the rule Indirect Proof (IP) to such conclusions.

Another lesson we can draw from the law for negation as a premise is that a reductio argument with a negative premise ¬ φ is valid if and only if the sentence φ is entailed by whatever other premises there are. This tells us that φ can be safely introduced as a lemma even if we drop ¬ φ from our active resources. The rule implementing this idea, Completing a Reductio (CR) serves as our rule for exploiting negative resources. It applies only to reductio arguments but the availability of IP insures that any gap will eventually turn into a gap in a reductio argument (unless it closes before that point). Since CR, by dropping a resource ¬ φ and adding a goal φ has an effect opposite to that of IP, we must apply them to different sentences φ to avoid going in circles. So, just as IP is limited to atomic sentences, CR is limited to negations of non-atomic sentences.

The rule CR can lead us to set as goals any lemmas we need in order to use negations in completing reductio arguments. It therefore eliminates any need for LFR. The rule Adj is also no longer needed (though still sometimes useful) since the rules CR and Cnj will lead us to identify and prove any lemma that Adj would introduce. Indeed, derivations for arguments involving conjunction can now be constructed by simply letting the rules guide us.