Introdução de Teses

$${\mathbb{T}}^{+}$$

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

Introdução de Teses (${\mathbb{T}}^{+}$)

$${\mathbb{T}}^{+}:\left\{\left[H⊢p\right],H\right\}⊢p$$ ou $$\frac{\begin{array}{cc}\boxed{\begin{array}{c}H\\ ⋮\\ p\end{array}}& H\end{array}}{p}\left({\mathbb{T}}^{+}\right).$$

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