$A⇒(B \lor C)$ and $[(A \Rightarrow B) \lor (A \Rightarrow C)]$

Question

[(A⇒ B∨C)] ⇒ [A⇒(¬B⇒C)] ⇒[(A⇒¬B)⇒(A⇒C)] ⇒ [¬(A⇒¬B)∨(A⇒C)]⇒[(A∧B)∨(A⇒C)]

[(A⇒B)∨(A⇒C)] is equivalent to A⇒(B∨C).

Can I prove [(A∧B)∨(A⇒C)] ⇒ [A⇒(B V C)]? or is there problem in the proof above

Please don't use truth table to prove. But only deduction rules. A∨B by definition ¬A⇒B Deduction rules:

1) A⇒(B⇒ A)

2) [A⇒(B⇒C)]⇒[(A⇒B)⇒(A⇒C)]

3) [A⇒B]⇒ [¬B⇒¬A]

Answer 1

For the part:

$[(A∧B)∨(A⇒C)]⇒[A⇒(B∨C)]$

we first replace $\lor$ and $\land$ with their definition in terms of $\lnot$ and $⇒$:

$A∨B$ stands for $¬A⇒B$ and $A∧B$ stands for $¬(A⇒¬B)$.

Applying them to the above formula, we get:

$[(A⇒¬B)⇒(A⇒C)]⇒[A⇒(¬B⇒C)]$.

In addition, we assume that we have available the Deduction Th, that is provable (together with $A ⇒ A$) from A1) and A2) only.

---

1) $[(A⇒¬B)⇒(A⇒C)]$ --- assumed [a]

2) $A$ --- assumed [b]

3) $¬B$ --- assumed [c]

4) $¬B⇒(A⇒¬B)$ --- axiom A1)

5) $A⇒¬B$ --- from 3) and 4) by Modus Ponens

6) $A⇒C$ --- from 1) and 5) by Modus Ponens

7) $C$ --- from 2) and 6) by Modus Ponens

8) $¬B⇒C$ --- from 3) and 7) by Deduction Th, discharging [c]

9) $A ⇒(¬B⇒C)$ --- from 2) and 8) by Deduction Th, discharging [b]

10) $[(A⇒¬B)⇒(A⇒C)]⇒[A⇒(¬B⇒C)]$ --- from 1) and 9) by Deduction Th, discharging [a].