Rule of Theorem Introduction

Definition

We may introduce, at any stage of a proof (citing TI), a theorem already proved, or a substitution instance of such a theorem, together with a reference to the theorem that is being cited.

Proof

This theorem is a corollary of the Rule of Sequent Introduction.

$\blacksquare$

Application

Using this rule, we can use theorems that we have derived in order to shorten proofs which may otherwise be long and unwieldy.

Sources

• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 4$