proof verification for natural deduction Could someone please let me know if I got the following natural deduction correct for the following formula 
(p ∧ q) ⇒ r ├ p ⇒ (q ⇒r)
1       (p ∧ q) ⇒ r    assump 0
2        p ├ (q ⇒r)    
2.1      p              assump 2.1
2.2      q ├ r         
2.2.1    q             assump 2.2
2.2.2    r             ⇒E 1,2.2
2.3      q⇒r          ⇒I 2.2
3        p⇒(q⇒r)      ⇒I 2, 2.3

 A: The notation is a bit weird to me. Does 2. announce what you're going to prove?
And you need an explicit step introducing $p \land q$ in the system I was taught.
The rest seems fine.
So in my notation:


*

*$(p \land q) \Rightarrow r$  (assumption/axiom)

*$p$                           (assumption)

*$q$ (assumption)

*$p \land q$ (from 2 and 3)

*$r$ (from modus ponens, 4 and 1)

*$q \Rightarrow r$ and 3 is dropped. (Introduction of $\Rightarrow$)

*$p \Rightarrow (q \Rightarrow r)$ and 2 is dropped (Introduction of $\Rightarrow$ again).


Proof complete, as the only undropped assumption is the "axiom" on the left hand side of $\vdash$. 
A: I agree with Henno Brandema about the need for a step that derives $p ∧ q$.
This answer primarily shows that there are proof checkers one can use for Fitch-style natural deduction.  Here is how the proof would look in the proof checker associated with the forallx text. Links to these are given below.

The reason one needs line 4 is to reference it in line 5 for conditional elimination (→E). A line for both the conditional (line 1) and the antecedent (line 4) are needed to derive the consequent (line 5). 
Software allows one to get verification checks as often as one wants. The cost is to use the particular input requirements for the software such as using capital letters for sentence variables. 

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
