Order of precedence If I write
$$a \to b \lor c \Longleftrightarrow \neg (b \lor c) \to a$$
is it parsed as
$$a \to (b \lor c \Longleftrightarrow \neg (b \lor c)) \to a$$
or
$$(a \to b \lor c) \Longleftrightarrow (\neg (b \lor c) \to a)$$
What about
$$a \to b \lor c \Longrightarrow \neg (b \lor c) \to a$$
In other words, what is the order of precedence between $\Longrightarrow, \Longleftrightarrow, \Longleftarrow$ and $\longrightarrow, \longleftrightarrow, \longleftarrow$?
 A: If you have both $\to$ and $\Rightarrow$ and the similar operators derived from them, then one of those is presumably an object-level connective, while the other is a meta-logical relation. From there, it would be clear which statements are nonsensical and thus a precedence can be deduced.
In particular, I suspect in the case your describing (but notation is definitely not standardized), $\iff$ is a meta-logical relation and it might be better to write something like $$\vdash a\to b\lor c \iff \vdash \neg(b\lor c)\to a$$ This would more explicitly state that the provability of the left-hand side is equivalent to the provability of the right-hand side. At any rate, if $\iff$ is meta-logical, then $$a\to (b\lor c\iff \neg(b\lor c))\to a$$ simply doesn't make any sense. $(b\lor c \iff \neg(b\lor c))$ is simply not a well-formed formula.
An analogy would be an algebraic expression like:
$a-bc = -bc + a$. We don't need to know the precedence between $=$ and $-$/$+$ to tell that $a-(bc = -bc) +a$ is not the intended parsing as it is nonsensical. Continuing the analogy, $(bc = -bc)$ is not an algebraic expression.
To the extent the precedence is specified, these "meta-logical" operations are given lower precedence than the object-level connectives.
