Introdução de Teses

$$\Huge \ndITese $$

Esta regra permite usar provas anteriores como regras: se previamente foi provado que $H \vdash p$ e na prova actual ocorrem todas as hipóteses de $H$ então $p$ é uma conclusão.

Introdução de Teses ($\ndITese$)

$$\Large \ndITese: \cbr{\sbr{H \vdash p}, H} \vdash p $$ ou $$\Large \ndrule{\ndsub{H \cr \vdots \cr p} & H}{p}{\ndITese}. $$

A sub-prova $H \vdash p$ é descartada na aplicação desta regra.