Skip to content
Free public beta until December 4, 2026: every course is open, no card needed. After that, the first chapter of each course stays free and full access is a one-time $39 ($19 for up to 100 founding members chosen for helpful feedback). Your progress is kept. How the beta works

Recipe

Prove an if–then with a subproof

Use when: the goal, or a line you need, has an if–then arrow as its main connective

Goal: the conditional written at the outer level, justified by conditional introduction on a closed subproof

Taught in Subproofs and conditional introduction

Quick recipe

  1. Assume the antecedent
  2. Work toward the consequent inside
  3. Finish the subproof on the consequent
  4. Step out and cite the whole range
  5. Never cite inside lines again
  1. 1

    Split the goal A \to B at its main arrow. Open a subproof whose first line is A, cited AS.

    Example

    Goal P \to (P \wedge Q): the antecedent is P, so line 2 is "│ P," cited AS.

    Why: \toI turns a subproof from A to B into A \to B, so the subproof has to start from A itself.

  2. 2

    Use any available line: the premises, lines of any subproof still open around you, and earlier lines of this one.

    • the consequent is itself an if–then — open a second subproof inside this one and run this recipe again.
    • the consequent is already available above — copy it in with R.

    Why: inside the subproof the assumption is in force, along with everything established outside it.

  3. 3

    The last line of the subproof must be B itself, symbol for symbol.

    Why: \toI reads the consequent off the subproof's last line.

  4. 4

    On the next line, back one level out, write A \to B and cite "\toI i–j," from the assumption's line to the last line.

    Example

    Line 5 is P \to (P \wedge Q), cited "\toI 2–4."

    Why: a range stands for the whole piece of what-if reasoning, and the assumption is discharged as it closes.

  5. 5

    From here on, lines i through j are off limits one at a time.

    Why: they depended on a supposition that is no longer in force.

Common mistakes

  • Carrying a line out of a closed subproof with R or by citing it.
  • Ending the whole proof inside a subproof.
  • Citing only part of a subproof, like 3–4 when it runs to 5.
  • Writing the conditional backward: the assumption is always the antecedent.