Teórico de Deducción Natural - Lógica de Primer Orden

Hola, hoy me surgio la siguiente duda:

Suponer que tengo la estructura $\langle \mathbb{N}, Par, Primo\rangle$ y quiero demostrar que $(\forall x)(P_1(x) \wedge P_2(x) \rightarrow x =' \bar{2} )$ que es equivalente a decir $(\forall x)(Par(x) \wedge Primo(x) \rightarrow x =' \bar{2} )$.

Ahora, he podido llegar hasta aqui en la demostracion pero no se como seguir: 

Mi pregunta es: ¿Como puedo continuar la derivacion para concluir que efectivamente si un numero es primo y par, entonces efectivamante es dos?