I agree with Graham Kemp's answer. I am adding a proof using a Fitch-style natural deduction proof editor and checker.
Two lines can be removed from the proof if I use a recommendation in the comments from Graham Kemp:
Just use the core rules of inference: assume Rba, to derive Rab ˄ Rba
and thus Raa, which contradicts ¬Raa so therefore deducing ¬Rba.
Here is the alternate proof:
Graham Kemp offered another suggestion which shortened the length of the proof and perhaps made it more understandable to a reader:
That checker explicitly lists ~E and ~I rules in the Basic Rules
column. You can surely use them.
I rearranged the universal eliminations to get this new version:
The premises are in the first two lines.
In lines 3 to 6 I use universal elimination (∀E) to replace the quantified variables, x, y and z, with the names, a and b. See Chapter 32, "Basic Rules for FOL" in forall x: Calgary Remix for a discussion. In particular I select names that will make the goal easy to reach: x becomes a, y becomes b, and z becomes also a.
Since the goal is a conditional I will need to start a subproof with an assumption that is the antecedent of the conditional I want to derive. If I can derive the desired consequent then I can close the subproof discharging the assumption and introduce the desired conditional. This is done in line 7 to 13.
To complete the proof I use universal introduction (∀I) in lines 14 and 15 to reach the final goal completing the proof.
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, Winter 2018. http://forallx.openlogicproject.org/