Biconditional Introduction in natural deduction

I'm working on a first-order logic question and I'm a little stuck as to what I should be assuming in my first subproof (this is always my problem). I'm supposed to prove this biconditional argument with no premises.

$P → (Q → R)) \leftrightarrow ((P ∧ Q) → R)$

I know that in order to do this, I need to prove that [P → (Q → R))] → [((P ∧ Q) → R)] ^ [((P ∧ Q) → R)] → [P → (Q → R))].

If I'm starting with my first subproof assuming P → (Q → R)), what is the next thing I need to assume so I can end up proving ((P ∧ Q) → R)? This is my thought process, but I get stuck at the point where I need to prove a →Intro.

P → (Q → R))
P
Q→R  →Elim 1
Q
P^Q  ^Intro 2,4
R  →Elim 3,4

After this I'm not quite sure what to do - how can I isolate it out so that R is the consequence of both P and Q?

• "If I'm starting with my first subproof assuming $P → (Q → R))$, what is the next thing I need to assume so I can end up proving $(P ∧ Q) → R$?" One thing you can do, one sensible thing you can do, is start a new subproof with $P\land Q$ as premise. – Git Gud Oct 10 '14 at 16:57
• By the way, the title is odd. Don't you mean biconditional introduction? – Git Gud Oct 10 '14 at 17:12
• Hm, I see what you're saying - I've edited the title. I'll give your suggestion a try and let you know how I make out! – Alonninos Oct 10 '14 at 17:14

Okay, now I've tackled the first subproof. Thanks for your help! This is what I got.

(P→(Q→R))
(P^Q)
P  ^Elim2
Q  ^Elim2
(Q→R)
R  →Elim 4,5
((P^Q)→R)  →Intro 2-6

• The last line is at the wrong level, but you got it. – Git Gud Oct 10 '14 at 20:22

It seems you really got it. Indeed, for a formal derivation using natural deduction in the general case, we just need to observe the logical form of the goals and decide which rules to use.

In your particular case, the statement you want to prove has the form of a biconditional $\phi \leftrightarrow \psi$, so we just have to prove that $\phi \rightarrow \psi$ and $\psi \rightarrow \phi$ holds first and appy the biconditional introduction rule:

$\frac{\frac{D}{\phi \rightarrow \psi}, \frac{D'}{\psi \rightarrow \phi}}{\phi \leftrightarrow \psi}$

Now we just observe the logical form of $\phi$ and $\psi$ and proceed with the other steps.