Next: Selecting, Previous: Connectives, Up: Basic Usage

### 4.3 Adding Sentences

Hitting `Ctrl+J` adds a conclusion to the proof. A conlusion is always added after the current line, or, if the line is a premise, then the conclusion is added after the last premise. If the current line is a conclusion, then it is highlighted in cyan. Hitting `Ctrl+P` adds a premise to the proof. A premise will always be added after the last premise. Pressing `Ctrl+B` adds a subproof to the proof. When in a subproof, a conclusion will always be added within the subproof. The first line of a subproof does not require a rule, but instead acts as a premise. Pressing `Ctrl+D` ends the current subproof. This creates a new conclusion just after the subproof.