Are the two Or-Elims equivalent? 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?
 A: No. Write $\triangledown$ for our wannabe disjunction, so we have the rule $\varphi\triangledown\psi,\neg\varphi\vdash\psi$ (and presumably we have $\varphi_i\vdash\varphi_1\triangledown\varphi_2$ as well). Then, to make use of the $\varphi\triangledown\psi$ assumption in $\varphi\triangledown\psi,\varphi\to\chi,\psi\to\chi\vdash\chi$ we need to be able to prove $\neg\varphi$. There is simply no reason this would be provable.
This is even more evident with a computational interpretation. Here's what the beginning of a proof attempt would look like in Agda:
data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

postulate WOr : Set → Set → Set
postulate Left : {φ ψ : Set} → φ → WOr φ ψ
postulate Right : {φ ψ : Set} → ψ → WOr φ ψ
postulate wOrElim : {φ ψ : Set} → WOr φ ψ → ¬ φ → ψ

orElim : {φ ψ χ : Set} → WOr φ ψ → (φ → χ) → (ψ → χ) → χ
orElim wor l r = r (wOrElim wor (λ x → ? (l x)))

There is no obvious choice of what to put for the ?. Computationally, there's no way to exfiltrate the $\chi$ l produces. In the computational interpretation of classical logic, Peirce's law gives us essentially a throw/catch mechanism so we could implement orElim in a made-up, classical version of Agda with something like:
orElim : {φ ψ χ : Set} → WOr φ ψ → (φ → χ) → (ψ → χ) → χ
orElim wor l r = try {r (wOrElim wor (λ x → throw (l x)))} catch(c) { c }    

This isn't a proof that it is impossible, of course. Maybe there's a clever program to do it that I didn't think of. In practice, though, programming experience combined with the computational interpretation of, particularly, intuitionistic logic makes it fairly easy to recognize that there are no data flow paths. As such, things which aren't intuitionistically provable become relatively self-evident.
If you did want to prove that you can't derive 2 from 1, you'd need to do something like an induction on the derivations, or you can make a counter-model, e.g. a topological model.
A: 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}$$
