Conditional Proof and lemmas I'm trying to solve a problem of propositional logic. The problem is this:
$(H\vee P \vee L) \wedge (¬H \Rightarrow ¬P \vee ¬L ) \wedge (¬L\Rightarrow ¬P ) \wedge ¬H \Rightarrow L$
So I'm solving this problem through a conditional proof where I assume the antecendent and prove the consequent. In order to do this I proposed a lemma:
Lemma 1: $¬P$
$¬H \Rightarrow ¬P \vee ¬L$
$=\langle Def \Rightarrow \rangle $
$¬¬H \vee ¬P \vee ¬L$
$=\langle Double ¬\rangle $
$H \vee ¬P \vee ¬L$
$=\langle \text{Assumption: } ¬L\Rightarrow ¬P \rangle $
$H \vee ¬P \vee ¬P$
$=\langle \text{Assumption: } ¬H \text{ is true then } H \text{ is false }\rangle $
$false \vee ¬P \vee ¬P$
$=\langle  \text{Identity }\vee\text{ and Idempotency}\rangle $
$¬P$
My first question is: Is valid to apply this assumption in the way that I did: $\langle\text{ Assumption: }¬L\Rightarrow ¬P \rangle $ and just replace ¬L by ¬P? I know Modus Ponens but don't know if it's valid in this case.
If it is valid, can I always do this? If it's not, why?
My second question is: Now that I proved ¬P can I use it in another lemma by replacing it by true? Lemma 1 was enough to proof that ¬P is true?
Meaning:
Lemma 2: $L$
$H\vee P \vee L$
$=\langle \text{Lemma 1 : }¬P\equiv true, P\equiv false \rangle $
$H\vee false \vee L$
I want to know if this steps that I'm doing are valid or if there is another way to do them in a formal way.
(I don't know if this is relevant, but I'm studying with the book A Logical Approach to Discrete Math by David Gries and Fred Schneider).
Thank you.
 A: So, are you taking that first formula (the big conjunction) as hipotesis? In the affirmative case it is ok what you did when you replaced $\lnot L$ by $\lnot P$ in the disjunction but I can't see how from $H \lor \lnot P \lor \lnot P$ whic is equivalent to $H \lor \lnot P$, you conclude $\lnot P$.
For the second lemma, if you have already proved $\lnot P$ and you assume $H \lor P \lor L$ then it follows $H \lor L$
A: Here are the questions:

My first question is: Is valid to apply this assumption in the way that I did: ⟨ Assumption: ¬L⇒¬P⟩ and just replace ¬L by ¬P? I know Modus Ponens but don't know if it's valid in this case. If it is valid, can I always do this? If it's not, why?

There is no rule in the proof checker that I am using that would permit that substitution. So I would have to try something different to derive $¬P$ (or find another proof checker).  So, the step would not always be valid. It would depend on the rules one has available.
Here is what I would do:

I would use modus ponens (conditional elimination: →E) and then check the cases on line 5. In each case I would need to derive $¬P$.

My second question is: Now that I proved ¬P can I use it in another lemma by replacing it by true? Lemma 1 was enough to proof that ¬P is true?

One could use $¬P$ to continue the proof to derive $L$.  Here is one way to do that.  I added $¬P$ to the premises to get the following:

The DS is disjunctive syllogism.  Note that after combining these two proofs together, it would take only 11 lines in this proof checker to derive $L$ counting four lines to state the premises. It may not be worth breaking this up into two parts.
The above proofs would be another way to approach the problem.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
