Completing a logical transformation.

Question

So I have a problem where I need to solve the first part of an implication so that it works with the second part.

https://i.stack.imgur.com/xx5bE.jpg
This is the problem as given to me.

What i have gotten up to now is this:
(P ∧ Q → P) → ((P ∧ Q) ∨ R → P ∨ R)
←
P ∨ R → S

https://i.stack.imgur.com/LbEax.jpg
The three laws that are use are included on this page.
I have checked with prover9/mace4 and this transformation is valid, but I am unsure if it is actually the correct transformation.

Answer 1

I'm not sure if I understand your task correctly.

(EDIT: Apparently I really didn't - see comments)

Anyway, I made some substitutions using the definitions given in your first link:

1. $(p \wedge q) \wedge p \rightarrow (p \wedge q)$
2. $(p \wedge q) \rightarrow p \rightarrow ((p \wedge q) \vee r \rightarrow p \vee r)$
3. $(((p \wedge q) \vee r) \rightarrow (p \vee r)) \rightarrow (((p \vee r) \rightarrow s) \rightarrow (((p \wedge q) \vee r)\rightarrow s))$

Using those substitutions as assumptions, we could continue transforming as follows:

4. $(((p \wedge q) \wedge p ) \vee r) \rightarrow ((p \wedge q) \vee r)$ (1, 4.5)
5. $((p \wedge q) \vee r) \rightarrow ((p \wedge q) \vee r)$ (4, 3.92b)
6. $((p \wedge q) \vee r) \rightarrow (p \vee r)$ (5, 3.92b)
7. $((p \vee r) \rightarrow s) \rightarrow (((p \wedge q) \vee r) \rightarrow s)$ (3, 6, 3.93)
8. $((p \wedge q) \vee r) \rightarrow (p \vee r)$ (5, 6, 3.99a)
9. $((p \vee r) \rightarrow s) \rightarrow ((p \vee r) \rightarrow s)$ (7, 8, 3.93)

...here's where it's me who gets stuck. What are the "Métathéorème" hiding at 3.100? Are you by any chance allowed to use $(p \rightarrow p) \rightarrow p$ ?