I'm having some trouble with my proof. I'm not sure if I am doing it correctly and I got stuck. The question is: Use rules of inference to show that if ∀x(P(x) → (Q(x) ∧ S(x))) and ∀x (P(x) ∧ R(x)) are true, therefore ∀x(S(x) ∧ R(x)) is true.
What I did was:
1.(P(x) ∧ R(x)) Premise
2.P(x) CS(1)
3.R(x) CS(1)
4.P(x) → (Q(x) ∧ S(x))) Premise
5.Q(x)∧ S(x) MP (2)(4)
6.Q(x) CS(5)
7.S(x) CS(5)
At this point I didn't know what to do. According to what I have done I proved that S(x) and R(x) are both true, but to be honest I don't even know if I did the proof correctly. If I did do it correctly, do I just add another statement saying how since both of them are true that (S(x) ∧ R(x)) has to be true? Any help would be appreciated, thank you for your time.
The problem with the OP's proof may be in missing steps to eliminate and introduce the universal quantifier. The other inference rules appear to be correct.
Here is a proof in a Fitch-style proof checker to show what might be done:
The premises are on the first two lines with universal quantifiers. I need to replace the variable $x$ with a name. I will use the name $a$ for both premises since they are true for all members of the domain. I perform the universal elimination on lines 3 and 4.
Then I proceed much as the OP did to arrive at line 9, $Sa \land Ra$.
To complete the proof I need to replace the name $a$ with the variable $x$ and so I introduce the universal quantifier and make that substitution on line 10.
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