Proof with disjunctive conclusion

Question

I'm after a natural deduction proof of the following sequent:

(P & Q) → R : (P → R) ∨ (Q → R)

The textbook I'm using says there is a 24 line proof, but the shortest I've managed is 29 lines. I've provided my proof below. Can anyone find the 24 line proof?

(In general, the proofs I'm overshooting on all seem to have disjunctive conclusions - so I'm wondering if there's some trick I'm missing for generating disjunctions.)

Thanks in advance!

---

Here's my 29 liner. Basically, I show ~(P → R) → (Q → R) [line 19] then get the conclusion from there by reductio.

EDIT 1: I've added dependency numbers in curly brackets {}, to indicate the premises and assumptions each line depends on.

EDIT 2: As Bram28 helpfully points out, my proof system is Lemmon-style (in case other people find this thread useful).

1. (P & Q) → R Premise {1}
2. ~(P → R) Assume for conditional proof{2}
3. Q Assume for conditional proof{3}
4. ~P Assume for reductio{4}
5. P Assume for comditional proof{5}
6. ~R Assume for reductio{6}
7. P & ~R 5,6 &-Introduction{5,6}
8. P 7 &-Elimination{5,6}
9. P & ~P 4,8 &-Introduction{4,5,6}
10. ~~R 6,9 reductio{4,5}
11. R 10 double negation elimination{4,5}
12. P → R 5,11 conditional proof{4}
13. (P → R) & ~(P → R) 2,12 &-Introduction{2,4}
14. ~~P 4,13 reductio{2}
15. P 14 double negation elimination{2}
16. P & Q 3,15 &-Introduction{2,3}
17. R 1,16 modus ponens{1,2,3}
18. Q → R 3,17 conditional proof{1,2}
19. ~(P → R) → (Q → R) 2,18 conditional proof{1}
20. ~((P → R) ∨ (Q → R)) Assume for reductio{20}
21. P → R Assume for reductio{21}
22. (P → R) ∨ (Q → R) 21 v-Introduction{21}
23. ((P → R) ∨ (Q → R)) & ~((P → R) ∨ (Q → R)) 20,22 &I{20,21}
24. ~(P → R) 21,23 reductio{20}
25. (Q → R) 19,24 modus ponens{1,20}
26. (P → R) ∨ (Q → R) 25 v-Introduction{1,20}
27. ((P → R) ∨ (Q → R)) & ~((P → R) ∨ (Q → R)) 20,26 &I{1,20}
28. ~~((P → R) ∨ (Q → R)) 20,27 reductio{1}
29. (P → R) ∨ (Q → R) 28 double negation elimination{1}

Answer 1

I can do it in 21 steps ... the proofs by contradiction work a little different in the system I use, which is why those steps don't check out, but I think the proof below conforms to your rules: