Are the two Or-Elims equivalent?

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.