(s → p) ∨ (t → q) entails (s → q) ∨ (t → p) natural deduction Hey guys I am stuck on this proof $(s \rightarrow p) \lor (t \rightarrow q)$ entails $(s \rightarrow q) \lor (t \rightarrow p)$
using natural deduction to prove it.
I used the or elimination in order to split up the two brackets, but I can't get any further...
Can anybody help me out on this one?
 A: $(s → p) ∨ (t → q)$
$( \neg s ∨ p) ∨ (\neg t ∨ q)$
$\neg s ∨ p ∨ \neg t ∨ q$
$\neg t ∨ p ∨  \neg s ∨ q$
$(\neg s ∨ q) ∨ (\neg t ∨ p)$
$(s → q) ∨ (t → p)$
A: 1) $(s → p) ∨ (t → q)$ --- premise
2) $(s → p)$ --- assumed [a1] for 1st $∨$-elim
3) $\vdash p \lor \lnot p$ --- LEM
4) $p$ --- assumed [b1] for 2nd $∨$-elim
5) $t \to p$ --- from 4) by $\to$-intro

7) $(s → q) ∨ (t → p)$ --- from 5) by $\lor$-intro

8) $\lnot p$ --- assumed [b2] for 2nd $∨$-elim
9) $s$ --- assumed [c]
10) $p$ --- from 9) and 2) by $\to$-elim
11) $\bot$ --- from 8) and 10)
12) $q$ --- from 11) by $\bot$-rule
13) $s \to q$ --- from 9) and 12) by $\to$-intro, discharging [c]

14) $(s → q) ∨ (t → p)$ --- from 13) by $\lor$-intro.

Now, from 4-7 and 8-14 and 3, by $\lor$-elim (the 2nd one) we derive :


15) $(s → q) ∨ (t → p)$ --- discharging temporary assumptions [b1] and [b2].


16) $(t → q)$ --- assumed [a2] for 1st $∨$-elim
and we have to repeat the same derivation above, concluding by $\lor$-elim (the 1st one) with :


17) $(s → q) ∨ (t → p)$ --- discharging temporary assumptions [a1] and [a2].


Thus :


$(s → p) ∨ (t → q) \vdash (s → q) ∨ (t → p)$ --- from 1), 2-15) and 16-17).



Note that the use of LEM in the proof has the role of the equivalence between  $p \to q$ and $\lnot p \lor q$ (see other answer), in the sense that, in order to prove $(p \to q) \leftrightarrow (\lnot p \lor q)$ with Natural Deduction, we have to use rules like RAA or DN that are equivalent to LEM.
