Database: Conditional elimination

Theorem 84: Conditional elimination/Modus ponens (inference rule)

Given that \phi holds and the implication \phi \Rightarrow \psi holds, we may infer \psi holds: \cfrac{\vdash \phi \quad \vdash (\phi \Rightarrow \psi)}{\vdash \psi}.

Proof: Assume the negation \neg \psi . Since \phi holds, conjunction introduction tells us that the conjunction \phi \wedge \neg \psi holds. Thus \neg \psi entails \phi \wedge \neg \psi .

But \phi \Rightarrow \psi is short for \neg (\phi \wedge \neg \psi) , which holds by our second premise. By weakening, \neg \psi entails \neg (\phi \wedge \neg \psi) . We thus get by negation introduction that \neg \neg \psi holds. By double negation elimination, we conclude \psi holds. \square

This database entry builds on the following:

  1. Definition: Conjunction
  2. Definition: Negation
  3. Definition: Implication
  4. Terminology: Inference, entailment
  5. Terminology: Inference rule
  6. Inference rule: Conjunction introduction
  7. Theorem: The weakening rule
  8. Inference rule: Negation introduction
  9. Inference rule: Double negation elimination