We have:
- $\varphi \lor \psi, \neg \varphi \vdash \psi$
- $\varphi \lor \psi, \varphi \to \chi, \psi \to \chi \vdash \chi$
Using $2$ and explosion (ex falso), one can prove $1$:
- $\varphi \lor \psi$ [premise]
- $\neg \varphi$ [premise]
- $\varphi$ [assumption]
- $\bot$ [contradiction 2 3.1]
- $\psi$ [explosion]
- $\varphi \to \psi$ [$\to$intro 3.1-3.3]
- $\psi$ [assumption]
- $\psi \to \psi$ [$\to$intro 5.1-5.1]
- $\psi$ [$\lor$elim 1 4 6]
However, can one prove $2$ from $1$ using other intuitionist rules?
You cannot constructively prove Proof By Cases from the suggestion Or-Elim rule. Consider the following valuations (found by my computer):
$$\begin{array} {cc|c} A & B & A \to B \\ \hline 1 & 1 & 1 \\ 2 & 1 & 1 \\ 3 & 1 & 1 \\ 1 & 2 & 2 \\ 2 & 2 & 1 \\ 3 & 2 & 1 \\ 1 & 3 & 3 \\ 2 & 3 & 3 \\ 3 & 3 & 1 \\ \end{array}$$
$$\begin{array} {c|c} A & \lnot A \\ \hline 1 & 3 \\ 2 & 3 \\ 3 & 1 \\ \end{array}$$
$$\begin{array} {cc|c} A & B & A \lor B \\ \hline 1 & 1 & 1 \\ 2 & 1 & 1 \\ 3 & 1 & 1 \\ 1 & 2 & 1 \\ 2 & 2 & 1 \\ 3 & 2 & 2 \\ 1 & 3 & 1 \\ 2 & 3 & 2 \\ 3 & 3 & 3 \\ \end{array}$$
And the following logic $L$:
$$\begin{array} {ll} \text{Axiom Schema:} & \\ \hline A \to B \to A & \text{Weakening} \\ (A \to B \to C) \to (A \to B) \to (A \to C) & \text{Conditional Modus Ponens} \\ \hline (A \to B) \to (A \to \lnot B) \to \lnot A & \text{Negation Propagation} \\ A \to \lnot A \to B & \text{Explosion} \\ \hline A \to (A \lor B) & \text{Or Intro 1} \\ A \to (B \lor A) & \text{Or Intro 2} \\ (A \lor B) \to \lnot A \to B & \text{Disjunctive Syllogism 1} \\ (A \lor B) \to \lnot B \to A & \text{Disjunctive Syllogism 2} \\ \hline \text{Inferences:} & \\ A, ~ (A \to B) \vdash B & \text{Modus Ponens} \\ \end{array}$$
Taking $1$ as the "true" value, each axiom schema is a tautology; and for modus ponens, implication has the property that if $A = 1$ and $(A \to B) = 1$ then $B = 1$. So every provable statement is also a tautology.
However, Proof By Cases, $P(A, B, C) = (A \lor B) \to (A \to C) \to (B \to C) \to C$, is not a tautology, specifically $P(2, 2, 2)\ne 1$. So it is not provable.
However, I suspect that replacing the negation schemas with the classical schemas $(\lnot A \to \lnot B) \to B \to A$ (or equivalent multiple rules for sanity's sake) leads to the Proof By Cases being provable since I've seen it in several logic publications.
KennyLau found the classical proof in a comment:
$$\begin{array} {rll} 1 & X \lor Y & \text{Premise} \\ 2 & X \to Z & \text{Premise} \\ 3 & Y \to Z & \text{Premise} \\ % 4 & \quad \quad \lnot Z & \text{Assumption} \\ 5 & \quad \quad \quad \quad Y & \text{Assumption} \\ 6 & \quad \quad \quad \quad Z & \text{Imp-Elim 3,5} \\ 7 & \quad \quad \lnot Y & \text{Contradiction of assumption 5, with 4 and 6} \\ 8 & \quad \quad X & \text{Needs a name, from 1 and 7} \\ 9 & \quad \quad Z & \text{Imp-Elim 2 and 8} \\ 10 & \lnot \lnot Z & \text{Contradiction of assumption 4, with 4 and 9} \\ 11 & Z & \text{Double negation elimination of 10} \\ \end{array}$$