I agree with Hunan Rostomyan's answer using disjunction elimination (vE) as well as virmaior's comment, "vE seems painful this way. Fitch has never heard of disjunctive syllogism?"
Here is a proof that uses disjunctive syllogism. As a proof this also illustrates that one has to follow the rules for well-formed statements built into whatever proof checker one is using so it can generate an answer.
In my case, the Fitch-style proof checker refused to accept the premises or conclusion as well-formed in first-order logic without the "x" being quantified. So, I added universal quantification of "x" on the premises and conclusion. This required that I first eliminate the universal quantifier, then use disjunctive syllogism (DS) and then introduce the universal quantifier.
The proof checker I am using is not the same one the OP is using. This may introduce other differences. For example, I could not use notation such as "P(x)", but I had to use "Px".
Using truth-function logic this would be simpler:
For more information on the rules see forall x: Calgary Remix.
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/