Welcome to the forum.

The sequent A, ¬ϕ ⇒ B is true, by definition, if is true and A ⇒ B, ϕ is true iff is true. Here denotes the conjunction of all formulas in A, and denotes the disjunction of formulas in B. In the following, however, let's pretend that A is and B is .A, ¬ϕ ⇒ B iff A ⇒ B, ϕ

So, assume that is true; we need to show . Assume A. If is true, then the conclusion is true and we are done. If is true, then the first assumption implies B, so again the conclusion is true.

For the converse, assume is true; we need to show that is true. Assume A and . Then the first assumption implies . However, since is true, B is also true, as required.

Ultimately, each of the equivalences in your question corresponds to a tautology, which can be verified using a truth table. For example, (5) corresponds to .

Why do you refer to these sequents as "modal"? They seem to come from regular, not modal logic.