iris
Modus Ponens P → Q, P ⊢ Q
Modus Tollens P → Q, ¬Q ⊢ ¬P
Hypothetical Syllogism P → Q, Q → R ⊢ P → R
Disjunctive Syllogism P ∨ Q, ¬P ⊢ Q
De Morgan (1) ¬(P ∧ Q) ≡ ¬P ∨ ¬Q
De Morgan (2) ¬(P ∨ Q) ≡ ¬P ∧ ¬Q