The meaning of $p \Rightarrow q \Rightarrow r$

Question

I understand that $p \Rightarrow q \Rightarrow r$ isn't defined since it might mean one of 4 different sentences:

1. $p \Rightarrow (q \Rightarrow r)$
2. $(p \Rightarrow q) \Rightarrow r$
3. $(p \Rightarrow q)\land(q \Rightarrow r)$
4. $(p \Rightarrow q)\land(p\land q \Rightarrow r)$

1), 2) While the first two make sense, because in the notation $p \Rightarrow q \Rightarrow r$ we just add brackets, but outside of mathematical logic I haven't seen them used in proofs.

3) The third option is quite common though, for example, if $x\in\mathbb{R}$ then $$|x-2|<3\quad\Rightarrow\quad -3<x-2<3 \quad\Rightarrow\quad -1<x<5$$ Another example (from page 375 of the book P. Naudin, C. Quitté, Algorithmique algébrique avec exercices corrigés, 1992): Also in this book Proofs and Mathematical Reasoning there are plenty of examples of implication chains (eg. page 13-14).

4) I don't recall if I've seen the fourth option used anywhere, but it would be so useful if we could write proofs using this notation, for example: $$x<-y^3<-1 \quad\Rightarrow\quad x<-\sqrt{y} \quad\Rightarrow\quad x^2>-x\sqrt{y}$$ A simpler example: $$1<x<2 \quad\Rightarrow\quad x<3 \quad\Rightarrow\quad 1<x<3$$ We can't write $x<3 \Rightarrow 1<x<3$ of course, but it's at the end of the chain (in text proofs this is quite common though, I mean we almost never say all the things we use for the last implication, i. e. we usually state things in sort of a chain: "if this then that, if this then that, ..., therefore we get that").

EDIT. The question is about the 4th case. Is it used by any authors? Is there a different arrow (or other symbol) notation for the 4th case?

Answer 1

Using arrows informally in a string of implications $$ p_0\Rightarrow p_1\Rightarrow p_2\Rightarrow\ldots\Rightarrow p_n $$ I would take to mean starting with something true and going through the implications left-to-right, asserting the truth of all of these $$ p_0\land(p_0\Rightarrow p_1)\land(p_1\Rightarrow p_2)\land\ldots\land( p_{n-1}\Rightarrow p_n), $$ with the goal of asserting $p_0\Rightarrow p_n$. In other words "checking each step is correct" is being interpreted as the conjunction of the implications.