Here's a new rule of replacement:

        Repetition: P <-> P

        So far, we have had no need for this rule. But it will make
derivations simpler when using the new rule that follows.

        Consider the following problem:

        Derive P -> (P & Q) from

               1.   P -> Q                  Premise

        This argument is obviously valid, yet we cannot prove it using the
rules we have. Try it, and see for yourself.

        To prove it, we need a new rule. This rule is the rule of
conditional proof. It allows you to derive a conditional (i.e. an if-then
statement) if you can show that its consequent follows from its antecedent.
To do this, you assume the antecedent on a line, and you show that the
consequent follows from it. When you assume something in a proof, you
indicate that with the word "Assumption." Thus, our proof should look like
this so far:

               1.   P -> Q                  Premise
               2.       P                   Assumption

        Note that I indented the P when I assumed it. I did this to mark
off the scope of the assumption from the rest of the argument. When you
make an assumption, you begin a sub-proof within your proof. You cannot use
any conclusions you draw inside your sub-proof outside of it in the rest of
the proof. Let me finish this proof up, then I will explain why that is so.
The proof, in its entirity, looks like this:

               1.   P -> Q                  Premise
               2.       P                   Assumption
               3.       Q                   1, 2, MP
               4.       P & Q               2, 3, Conj.
               5.   P -> (P & Q)            2-4, CP

        CP, of course, stands for Conditional Proof. After I assumed P, I
showed that (P & Q) followed from it. I did this in lines 2 through 4.
Therefore, I indicated on line 5 that I derived it from lines 2-4 by CP.
When I drew my conclusion by CP, I closed off the scope of my assumption.
Therefore, I cannot infer anything more from those lines in this proof. For
instance, it would be wrong for me to use simplification to infer Q from
line 4 onto line 6. Consider, now, the following problem:

        Derive (P v Q) <-> (P & Q) from scratch

        As I will show later, we can derive tautologous conditionals and
biconditionals from scratch. This biconditional, however, is not
tautologous. So, we should not be able to derive it. We could prove it,
however, if we could derive lines from lines within closed assumptions. I
will demonstrate that as follows:

               1.       P & Q               Assumption
               2.       P                   1, Simp.
               3.       P v Q               2, Add.
               4.   (P & Q) -> (P v Q)      1-3, CP
               5.       P v Q               Assumption
               6.       P & Q               1, R (Illegal)
               7.   (P v Q) -> (P & Q)      5-6, CP
               8.   (P v Q) <-> (P & Q)     4, 7, Equiv.

        I derived line 6 from within the scope of the previously closed
assumption. By doing so, I derived a conclusion that I should not have been
able to derive. In order to avoid errors like this, you should never derive
lines from lines that are within the scope of a closed assumption.