==== <math>(\exists x)P(x), (\forall x)(\forall y)(P(x) \to Q(y)) \vdash (\forall y) Q(y)</math> ====
: {{#ev:youtube|C37Y-1vqRAY|||||start=810}}
==== <math>(\forall x)A(x), (\exists y)(A(y) \to B(y)), (\forall z)(A(z) \to C(z)) \vdash (\exists w)(B(w) \land C(w))</math> ====
: {{#ev:youtube|C37Y-1vqRAY|||||start=1152}}
==Dedução Natural para a Lógica de Primeira Ordem Clássica==