one-point rule

Hello all,

I'm not sure if anyone here has studied formal systems. I'm studying this module and now trying to simplify the following equation using one-point rule and other predicate logic.

Attachment 11053

I'm not sure what inference rule to use to simply before i can use one-point rule. Specially the implication rule. And of course this is using Z. Any help or a direction would be much helpful.

Thanks very much guys!

ssharish