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))
Q→R →Elim 1
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?