Modus Ponens
p
p → q
. . . . . . . . .
q
Modus Tollens
¬q
p → q
. . . . . . . . .
¬p
Hypothetical Syllogism
p → q
q → r
. . . . . . . . .
p → r
Disjunctive Syllogism
p ∨ q
¬p
. . . . . . . . .
q
Addition
p
. . . . . . . . .
p ∨ q
Simplification
p ∧ q
. . . . . . . . .
p
Conjunction
p
q
. . . . . . . . .
p ∧ q
Resolution
p ∨ q
¬p ∨ r
. . . . . . . . .
q ∨ r
Universal Instantiation
∀ x P(x)
. . . . . . . . .
P(c)
Universal Generalization
P(c) for an arbitrary, c
. . . . . . . . .
∀ x P(x)
Existential Instantiation
∃ x P(x)
. . . . . . . . .
P(c) for some element, c
Existential Generalization
P(c) for some element, c
. . . . . . . . .
∃ x P(x)