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

.

By we can take appropriate values such that

.

From and we obtain by modus ponens

.

From and we obtain by modus ponens

.

By we can take appropriate values such that

.

By we can take appropriate values such that

.

We prove first

.

For proving we prove, for arbitrary but fixed values,

Formula is proved because is an instance of it.