| 9402 | RAA: If assuming A will prove B∧¬B, then derive ¬A [Lemmon] |
| 9393 | A: we may assume any proposition at any stage [Lemmon] |
| 9399 | ∧E: Given A∧B, we may derive either A or B separately [Lemmon] |
| 9395 | MTT: Given ¬B and A→B, we derive ¬A [Lemmon] |
| 9396 | DN: Given A, we may derive ¬¬A [Lemmon] |
| 9397 | CP: Given a proof of B from A as assumption, we may derive A→B [Lemmon] |
| 9394 | MPP: Given A and A→B, we may derive B [Lemmon] |
| 9400 | ∨I: Given either A or B separately, we may derive A∨B [Lemmon] |
| 9398 | ∧I: Given A and B, we may derive A∧B [Lemmon] |
| 9401 | ∨E: Derive C from A∨B, if C can be derived both from A and from B [Lemmon] |
| 13500 | Conditional Proof: infer a conditional, if the consequent can be deduced from the antecedent [Hart,WD] |
| 14273 | Conditional Proof is only valid if we accept the truth-functional reading of 'if' [Edgington] |
| 10987 | Three traditional names of rules are 'Simplification', 'Addition' and 'Disjunctive Syllogism' [Read] |
| 13524 | Deduction Theorem: T∪{P}|-Q, then T|-(P→Q), which justifies Conditional Proof [Wolf,RS] |