==== <math>(\exists x)(\varphi_1 \lor \varphi_2) \dashv \vdash (\exists x)\varphi_1 \lor (\exists x)\varphi_2</math> ====
: {{#ev:youtube|C37Y-1vqRAY|||||start=1425}}
==== <math>(\exists x)(\forall y) \varphi \vdash (\forall y)(\exists x) \varphi</math> ====
: {{#ev:youtube|C37Y-1vqRAY|||||start=1701}}
==== <math>(\forall x)\neg\varphi \vdash \neg(\exists x)\varphi</math> ====
: {{#ev:youtube|C37Y-1vqRAY|||||start=1910}}
==Dedução Natural para a Lógica de Primeira Ordem Clássica==