Help in proving ∀x(¬A(x) → B(d)) ⊢ ∀xA(x) ∨ B(d) without using Disjunctive syllogism in the proof Stuck on a problem of ∀x(¬A(x) → B(d)) ⊢ ∀xA(x) ∨ B(d), however the system I am using does not allow me to use DS in the proof. Here is another method I tried, but it says that it's wrong on the last step. Anyone know how to go about solving this with just the basic rules for FOL and TFL natural deduction?
∀x(¬A(x) → B(d)):PR
-A(c)->B(d):AE 1
-A(c)/\-B(d):AS
-A(c):/\E 3
-B(d):/\E 3
B(d):->E 2,4
_|_:-E 5,6

-(-A(c)/-B(d)):-I 3-7
 -(A(c)\/B(d)):AS
    -A(c):AS
        -B(d):AS
        -A(c)/\-B(d):/\I 10,11
        _|_:-E 8,12
    B(d):IP 11-13
    A(c)\/B(d):\/I 14
    _|_:-E 9,15
--
    A(c):AS
    A(c)\/B(d):\/I 18
    _|_:-E 9,19
A(c):IP 10-16
-A(c):-I 18-20
_|_:-E 21,22

A(c)/B(d):IP 9-23
∀xA(x) ∨ B(d):AI 24
 A: Let $\phi$ be: $$(\neg A \implies B) \implies (A \lor B)$$
You want to prove that  $\phi$ is a tautology, using basic natural deduction rules.
\begin{align}
   (\neg A \implies B) \quad \neg A  &&\text{Assumption (1) (2) respectively}\\
\
   B \qquad \qquad&& \text{using implies elemination} \\
\
   (A \lor B) \quad \neg(A \lor B)&& \text{using or introduction, Assumption (3)} \\
\
   \bot  \qquad \qquad&& \text{using not elemination} \\
\
   A \qquad \qquad && \text{using contradiction elemination, eliminating assumption (1)} \\
\
    (A \lor B) \quad \neg(A \lor B)&& \text{using or introduction, same assumption (3)} \\
\bot  \qquad \qquad&& \text{using not elemination} \\
\
A \lor B \qquad \quad && \text{using contradiction elemination, eliminating assumption (3) two times}\\
 (\neg A\implies B)\implies A\lor B  &&\text{using implies introduction , eleminating assumption (1)}\\
\end{align}
Thus we proved $\vdash\phi$ without usign any assumption that is $\phi$ is a tautology (Note that all assumption where eliminated in the proof).
