The simplest application of a conditional.

Apply Modus Ponens twice to chain conditionals.

Extract a component from a conjunction.

Show that P ∧ Q implies Q ∧ P.

Weaken a fact into a disjunction.

Combine two facts into a conjunction.

Unpack a conjunction, then use a conditional.

Apply a nested conditional step by step.

Apply Modus Ponens three times along a chain of conditionals.

Pull a component from a conjunction, then apply a conditional.

Reach inside a nested conjunction to extract a deep component.

Apply the same premise in two different conditionals.

Turn each of two premises into a disjunction, then combine them.

Chain two conditionals into one using a subproof.

Every proposition implies itself.

Prove the classical contrapositive argument.

From a contradiction, anything follows.

Both antecedent and negated consequent give a contradiction with the conditional.

Strip a double negation.

Produce a conjunction inside a conditional.

If P implies R, then so does any stronger P ∧ Q.

A single false component makes the whole conjunction false.

Any proposition implies the conjunction of itself with itself.

If Q holds and P implies R, build a conditional that gives both.

Eliminate a disjunct using its negation.

Use ∨E to handle two symmetric cases.

A conditional is equivalent to its contrapositive.

Distribute conjunction over disjunction.

Show that P ∨ Q implies Q ∨ P using case analysis.

Negating a disjunction gives two separate negations.

P ∨ P contains no new information — both cases give P.

Factor a shared conjunct out of a disjunction.

Every proposition is either true or false — prove P ∨ ¬P from nothing.

Two separate negations together negate the whole disjunction.

A classical tautology: if P → Q implies P, then P holds outright.

Prove P by contradiction (classical reductio).