Discrete Math - Rules Of Inference Proof 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.
 A: 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
