Database: Reverse of conditional introduction

Proposition 99: Reverse of conditional introduction (inference rule)

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

Proof: Assume \phi . By conditional elimination, we infer that \psi holds. Thus, \phi entails \psi . \square

This database entry builds on the following:

  1. Definition: Implication
  2. Terminology: Entailment
  3. Terminology: Inference rule
  4. Theorem: Conditional elimination