>>14534
Yo la hice así (se entiende que la variable entre paréntesis, (x) significa "para todo x"):
1. ... (en esta línea el problema en
>>14534)
{2.Pz ; hipótesis 1
{3.(y)[Py-->Ny] ; hipótesis 1.1
4.Pz-->Nz ; instanciación universal de 3
5.Nz ; modus ponens de 2 con 4
6.Nz-->Oz ; instanciación universal de 1
7.Oz ; modus ponens de 5 con 6; hasta aquí llega hipótesis 1.1}
8.(y)[Py-->Ny]-->Oz ; prueba condicional del 3 al 7 hasta aquí llega hipótesis 1}
9.Pz-->((y)[Py-->Ny]-->Oz) ; prueba condicional del 2 al 8
10.(x)[Px-->((y)[Py-->Ny]-->Ox)] ; generalización universal de 9 ; QED