Assume [¬P∧(P∨Q)]. From "both x and y" as true, we may infer x as true. We may also infer y as true. So, we can infer ¬P as true, as well as (P∨Q) as true. Assume P true. Assume ¬Q true. Then since we have ¬P and P true, we may discharge the negation and infer Q. So, (P→Q) holds true. Suppose Q true. Then Q holds true. So, we can infer (Q→Q) holds true. Since (P∨Q), (P→Q), and (Q→Q) hold true, it follows that Q holds true. Since [¬P∧(P∨Q)] comes as the only assumption still in place, we may infer {[¬P∧(P∨Q)]→Q} as true as desired.
Via Polish notation, (P∨Q) can get rewritten as Apq, [¬P∧(P∨Q)] can get rewritten as KNpApq, and {[¬P∧(P∨Q)]→Q} can get rewritten as CKNpApqq. We can then use the following axioms to prove CKNpApqq as a theorem. By a relevant soundness meta-theorem, we'll have CKNpApqq as a tautology also.
A1 CpCqp - recursive variable prefixing - RVP
A2 CCpCqrCCpqCpr - self-distribution - SD
A3 CCNpKqNqp - negation out - No
A4 CKpqp - conjunction out left - Kol
A5 CKpqq - conjunction out right - Kor
A6 CpCqKpq - conjunction in - Ki
A7 CCpqCCrqCAprq - disjunction out - Ao
Via the relevant deduction meta-theorem which SD and RVP enable, we have conditional introduction as a derivable rule of inference, which I'll denote as Ci. The only other rule of inference I'll use is C-detachment or C-d
{C$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$.
1 hypothesis | KNpApq
2 Kol | CKNpApqNp
3 C-d 2, 1 | Np
4 Kor | CKNpApqApq
5 C-d 4, 1 | Apq
6 hypothesis || p
7 hypothesis ||| Nq
8 Ki ||| CpCNpKpNp
9 C-d 8, 6 ||| CNpKpNp
10 C-d 9, 3 ||| KpNp
11 Ci 7-10 || CNqKpNp
12 No || CCNqKpNpq
13 C-d 12, 11 || q
14 Ci 6-13 | Cpq
15 hypothesis || q
16 Ci 15-15 | Cqq
17 Ao | CCpqCCqqCApqq
18 C-d 17, 14 | CCqqCApqq
19 C-d 18, 16 | CApqq
20 C-d 19, 5 | q
21 Ci 1-20 CKNpApqq.