We prove by natural deduction.

For proving we prove, for arbitrary but fixed values,

.

We prove by the deduction rule.

We assume

and show

.

From and we obtain by modus ponens

.

From and we obtain by modus ponens

.

From by specialization we obtain

.

For proving , by , it suffices to prove

.

For proving we prove, for arbitrary but fixed values,