Conditional elimination

If we have a conditional and we have independently derived its antecedent, we may invoke its consequent. This is often referred to as Modus ponens (affirming the antecedent).

Strategies for constructing proofs in propositional logic
- Next we need to turn our attention to deriving \(L \lor A\). How can we obtain \(L\) ? Well it is contained within the first conjunct of the assumption on line 2. Again, we can get this through the application of Conjunction Elimination. Now, how do we get \(L\) from \((\lnot N \rightarrow L)\)? Well, we already have the antecedent \(\lnot N\) as an assumption on the first line, so we can use Conditional Elimination to derive \(L\). These two steps give us:
Formal proofs in propositional logic
- Conjunction Elimination