Before we prove some theorems, it is worth mentioning a few useful theorems and derived rules. They
are all solely based on propositional logic and temporal logic without chop and we omit their
proofs.
| ⊢ | f1 ⊃ f2, ,…, ⊢ fn−1 ⊃ fn ⇒ ⊢ f1 ⊃ fn | | ImpChain
|
| ⊢ | f1 ≡ f2, ,…, ⊢ fn−1 ≡ fn ⇒ ⊢ f1 ≡ fn | | EqvChain
|
| ⊢ | f1,⊢ f2,…,⊢ fn ⇒ ⊢ g, | | Prop
|
| where the formula f1 ∧ f2 ∧…fn ⊃ g | |
|
| is a substitution instance of a propositional tautology | | |