Trying to check whether a formal proof is correct Am having a little difficulty trying to formally prove a formula. I'm new to this so just trying to have a go and see where I get to. The formula I have is copied in below; 
     p ∧ r ⇒ q ∧ r , p ∨ r ⇒ q ∨ r |- p ⇒ q

I have had a go at it but I don't really know if I'm correct. I would be really grateful if someone could check for me. 
    1. p ∧ r ⇒ q ∧ r    Assumption 0
    2. p ∨ r ⇒ q ∨ r    Assumption 0
    3. p |- q   
   3.1 p                 Assumption 3
   3.2 r                 ∧-E from Line 1
   3.3 q                 ⇒-E from Line 1 & 2
    4. p ⇒ q             ⇒-I from Line 3.1 & 3.3

I would really appreciate it if anyone could show me if I'm going wrong. I'm not sure at all if I'm right or wrong. 
Thanks. 
 A: Your line 3.2 is wrong. You can't apply $\land$-elimination to line 1, because line 1 does not have $\land$ as its top-level connective; it should be parenthesized as $(p\land r)\Rightarrow(q\land r)$.
Line 3.2 is wrong too; neither of line 1 and 2 is identical to the left-hand side of the other wone. And in any case $q$ is not the right-hand side of either of 1 and 2; $\Rightarrow$-elimination can only conclude a formula that is to the right of a $\Rightarrow$ in its first premise.

It would probably help if you formulate a proof in informal English before you try writing down a formal one. It would go something like:

Since we have $p$, in particular $p\lor r$ and therefore, by the second assumption $q\lor r$. If $q$ is true, then we're done already; otherwise $r$ is true, so we have $p\land r$, and therefore by the first assumption $q\land r$. So in this case too, $q$ will hold.

A: 1) $p ∧ r → q ∧ r$ --- premise
2) $p ∨ r → q ∨ r$ --- premise
3) $p$ --- assumed [a]
4) $p ∨ r$ --- from 3) by $∨$-I
5) $q ∨ r$ --- from 4) and 2) by $→$-E.
Now we need $∨$-E (proof by cases) from 5):
6) $q$ --- assumed [b]
7) $p → q$ --- from 3) and 6) by $→$-I
8) $r$ --- assumed [c]
9) $p ∧ r$ --- from 3) and 8) by $∧$-I
10) $q ∧ r$ --- from 1) and 9) by $→$-E
11) $q$ --- from 10) by $∧$-E
12) $p → q$ --- from 3) and 11) by $→$-I.
Having derived $p → q$ from both 6) and 8), we can apply $∨$-E to 6)-7) and 8)-12) and 5), discharging [b] and [c], to conclude with:

$p → q$.

Thus:


$p ∧ r → q ∧ r, p ∨ r → q ∨ r \vdash p → q$.


