"Given p ⇒ q and q ⇔ r, use the Fitch system to prove p ⇒ r"? I'm having some difficulty understanding the Fitch system - could someone please break down and answer the aforementioned question for me?
I'm able to get to:


*

*p => q                  Premise 

*q <=> r                 Premise 2

*p                       Assumption    

*q                       Implication elimination 1,3

*q => r                  Biconditional elimination 2

*p => (q => r)           Implication introduction 3,5
My issue is that I don't know how to whittle 6. down into p=>r - I know the operation required could be called the inverse of implication distribution, but beyond that I'm stumped.
Help!
 A: What you want to show is an implication $p \to r$, so you know that the last thing to happen is likely an implication introduction:
| 3. p      (assumption)
...
| n. r      (?)
6. p -> r   (->I, 3-n)

For an implication introduction, you need to have derived $r$ form assumption $p$. You already have $p$ as an assumption in l. 3, so you need to derive $r$ in that subproof. Now what are the formulas in your proof which you could get $r$ from? You've got $q \to r$ on line 5. Given the other conclusions and assumptions you have up until there, how do you think you could combine them to derive $r$? It's just one additional step. Once you got that figured out, you're done.
A: Edit: Another answerer submitted a responce 30 seconds before mine, and their response does not give the entire answer, instead it gives a hint. As such I have marked my answer as a spoiler, which you can view by hovering your mouse over it if you wish to.

 Your proof is almost correct. Instead of making an implication introduction on line 6, make an implication elimination between 4 and 5 to arrive at $r$. Then perform your implication introduction to get $p\implies r$.

Full answer:

 \begin{align}1.&p => q&~Premise\\2.&q <=> r&~Premise\\3.&p&~Assumption\\4.&q&~Implication~elimination~1,3\\5.&q => r&~Biconditional~elimination~2\\6.&r&~Implication~elimination~4,5\\7.&p\implies r&~Implication~introduction~3,6\end{align}

A: Most likely your line 5 is incorrect. Typically, in a Fitch system, Biconditional elimination would be applied on two lines: one being the biconditional, and the second being one of the two sides of that biconditional, allowing you to infer the other side.
So, in this case, you'd infer $r$ from line 4 ($p \leftrightarrow r$) and 2 ($q$), and now the conditional introduction rule gives you exactly what you want.
