Prove P∧(Q∨R)→(P∧Q)∨(P∧R) from P∧(Q∨R) using Natural Deduction I am trying to prove  P∧(Q∨R)→(P∧Q)∨(P∧R) from P∧(Q∨R) using Natural Deduction.
Here is my attempt using JAPE application.


I am confused between step 3 and 4.
So I have Q∨R. When ever I apply V-elimination rule, I get this output below, so I get an output and I apply again V-elimination rule. It is like infinity

 A: not sure what you are trying to do but here the proof as I would do it: (but I don't use jape)
1  | |____ P & (Q v R)                           Assumption
2  | |     P                                     & elim 1
3  | |     Q v R                                 & elim 1
4  | | |__ Q                                     Assumption
5  | | |   P & Q                                 2,3 & intro 
6  | | |   (P & Q) v (P & R)                     5 v Intro
.  | | <-----------------------------------    end subproof
7  | | |__ R                                     Assumption
8  | | |   P & R                                 2,7 & intro 
9  | | |   (P & Q) v (P & R)                     8 v Intro
.  | | <-----------------------------------    end subproof 
10 | |     (P & Q) v (P & R)                     3, 4-6, 7-9 v elim
.  | <-------------------------------------    end subproof 
11 |       (P & (Q v R)) -> ((P & Q) v (P & R))  1-10 -> intro

A: I don't know the software you're using, but it looks like you've already committed to proving $(P\land Q)\lor(P\land R)$ by showing $P\land R$. However that won't work if the reason $P\land(Q\lor R)$ was true is that $P$ and $Q$ are true but $R$ is false.
Instead you need to do the $\lor$-elimination on $Q\lor R$ first, and in each branch of that you can then chose a $\lor$-introduction rule that matches the case you're in.
