This derivation has three premises.  Line 4 results from applying modus tollens to lines 2 and 3.  Line 2 is a conditional, and line 3 is the negation of the consequent of that conditional. So we inferred the negation of the antecedent of the conditional.  We get line 5 from lines 1 and 4 by disjunctive syllogism. Notice that our inferences can be drawn from any lines, not just our premises. Once a wff becomes a line of a derivation, we can appeal to it in any appropriate inference.

In contrast, the following is not a derivation:

There are several problems with this example, though it only takes one errant line to create a non-derivations. Like so much in logic, whether something is a derivation is an all or nothing affair. There are no "sort-of derivations."  Our premises are fine. Line 4 claims to be an inference by modus ponens of B from lines 1 and 3. But modus ponens works only when we have a conditional, and line 1 is a biconditional. In fact, we have no rules of inference covering biconditionals at all! (This is a limitation we will correct when we introduce the equivalence rules.)  So this example is a non-derivation in virtue of line 4 alone. But there is another problem.  Line 7 conjoins lines 3, 4 and 6. But our rule for conjoining allows us only to conjoin the wffs on two lines.  Another hint that 7 is problematic is that the inferred result is not a wff!

Several exercises are available to gain familiarity with the rules of inference and to construct derivations. The are as follows:

• Rules of Inference I

• Rules of Inference II

• Rules of Inference III

• Rules of Inference IV