# 17.4 →Intro and ↔Intro

It's probably no surprise that we have a formal rule that mirrors conditional proof. In fact we have two, since we need Intro and Elim rules for all our connectives, and →Intro and ↔Intro are the only rules we haven't created yet.

Can you figure out how →Intro should look, without us even telling you? Try this one:

1. P→(Q&R)

Thus,

2. P→Q

**→Intro:**Start a subproof that assumes the antecedent, and end the subproof with the consequent. Cite just the subproof with a dash.

Conditional proof works by temporarily assuming the antecedent, and getting to the consequent, and our mechanism for a temporary assumption is the subproof.

So to do →Intro for a conclusion like X→Y, start a subproof assuming X, and end the subproof with Y. That allows you to move out of the subproof and justify X→Y in the parent proof by citing →Intro;2-4. (Assuming the subproof was lines 2 to 4).

**Whenever your conclusion is a conditional, setting up an →Intro proof is always the easiest way to do it.**

Now try this one:

1. P→Q

2. Q→R

Thus,

3. P→R

Now let's try a hard one. This proof is like you did in section 17.2, but there you had R as a 4th assumption. But with just the first three assumptions, you can prove that if R, then S.

1. PvQ

2. (P&R)→S

3. (Q&R)→S

Thus,

4. R→S

This is a fun proof for a couple of reasons. First, it is a bit more complex that what we've been doing. But you've already done a simpler version of it, so we think you can figure it out.

Try to complete the proof now, without more help.

******

Pause

******

The second reason is because there are two good ways to do it, so you have to make a decision. You might see the disjunctive premise, and think: I should do proof by cases. That's great--that will work. Or you might see the arrow conclusion and think: I should do conditional proof. That's great too--it also works.

The fact is, you'll have to use both proof methods to do the proof, and you can do it in either order. However, we'll repeat a general rule that is quite helpful: conditional proof takes precedence over everything. Any time you have a conditional conclusion in a hard proof, starting first with conditional proof is the easiest way to go.

Here's one way to think about it. If you start with proof by cases, you'll have to prove your conclusion in each case. Since your conclusion is an arrow, you'll have to do two conditional proofs. But if you start with conditional proof, you'll only have to do one.

Now that you've heard more advice, go back and finish the proof if you didn't get it before. If you already got it, now see if you can do it the *other* way.

******

Pause: We really mean it.

******

Now that you've worked on it as much as you can, we'll show you our sketch, taking the easy way:

Now you can finish the proof in this practice problem.

Our finished proof looks like this:

Hopefully you already work out how to do it in the other order for practice. If so, here's the solution to check your work with:

**↔Intro:**to prove X↔Y, start a subproof with X and end it with Y, then start a separate subproof with Y and end it with X.

Lastly, we must cover ↔Intro. For that rule, all you need is two subproofs. Assume one side of the biconditional and get to the other, and vice versa.

The most important thing to know is that you do * not* actually prove the individual conditionals first, and use them to justify the biconditional. Instead, move straight from the subproofs to the biconditional.

Here's an example. This sentence is a tautology: (P&Q)↔(Q&P). That means you can prove it from no premises at all.

Let's give it a try.