# 19.1 -> Conclusions: Awesome!

When we covered hard proofs in BOOL, you learned to pay attention to the main connectives.

Each type of connective, as a premise or as a conclusion, dictated a plan. For example, when you have a conjunction premise, you bring down the conjuncts with &Elim. And when you have a conjunction conclusion, you first prove each side individually, and then build the conclusion with &Intro.

The good news is that everything you learned from BOOL still applies!

The good news is that everything you learned from BOOL still applies. You never have to unlearn anything in this book!

Now we just need to learn the characteristic plans for dealing with the new connectives of PROP, -> and <->.

When you have -> conclusion: always start a ->Intro proof!

The first case we’ll cover is when you have a conditional conclusion. When your conclusion is a wide-scope arrow, just start an ->Intro proof: assume the antecedent in a new subproof, and try to get to the consequent.

For example, prove this tautology: (P&Q&R)->Q.

This lesson is so powerful, we’ll create a general rule: whenever your conclusion is a wide-scope conditional, the idea to start an ->Intro proof is always the best way to go.

The ->Intro idea applies to intermediary conclusions as well.

Additionally, this point applies not just to your final conclusion, but to any intermediary conclusions that you are trying to prove as well.

For example, let’s say you are proving this tautology: (P->Q)->((P->~Q)->~P). When you use the ->Intro plan, you assume P->Q and try to get to (P->~Q)->~P.

Notice that now your new goal, (P->~Q)->~P, is also a wide-scope arrow. So what should you do?

The ->Intro plan! Start another subproof: assume the antecedent and try to get to the consequent.

Let’s try it.

Remember to check for a conditional conclusion in the rest of the proofs from this chapter. If it’s a wide-scope arrow, you know how to start the proof!