Conditionals and Implications Until recently, I wasn't aware of the subtle difference in $\to$ and $\implies$. I've read the previous answers, and want to put it all together to corroborate my understanding.
$P \to Q$ is a propositional statement formed by the binary logical connective $\to$ and two statements $P,Q.$ I see $P \to Q$ as a promise, thereby motivating its truth table where it's only false when $P$ is true and $Q$ is false.
Say, we are proving the theorem $$n\text{ is even}\implies n=2m\text{ for some integer }m.$$ Now, when we write at the end of our proof that $P \implies Q$, what we are saying is that if $P$ holds, then $Q$ also holds, if truth value of $P$ is 1, then truth value of $Q$ is also 1. That is, through our proof, we are denying there being any case of $P$ true and $Q$ false. So if I am to relate $P \implies Q$ to $P \to Q$, I'd say that $P \implies Q$ asserts that it cannot be the case that $P$ holds and $Q$ doesn't hold, thereby ultimately saying that $P \to Q$ is always true (including trivial vacuous cases), i.e. $P \to Q$ is a tautology.
$P \iff Q$ asserts if $P$ holds, then $Q$ also holds; and if $Q$ holds, then $P$ also holds. In relation to $P \leftrightarrow Q$, it says that $P \leftrightarrow Q$ is a tautology, i.e. $P \leftrightarrow Q$ is always true, thereby saying that the truth values of $P$ and $Q$ always go together as the same; and that it cannot be the case that truth values of $P$ and $Q$ are different. $P \iff Q$ is also called logical equivalence.
I've read that $\implies$ and $\iff$ are not connectives, but that they are making meta statements (statements about about propositions $P$ and $Q$). Are $\implies$ and $\iff$ just shorthand then for saying, "if you start with $P$, you can deduce $Q$" and "if you start with $Q$, you can deduce $P$" etc. ?
 A: 
when we write at the end of our proof that $P{\implies}Q,$ we are asserting that it cannot be the case that $P$ holds and $Q$ doesn't hold,

Yes.

thereby ultimately saying that $P \to Q$ is always true, i.e. $P \to Q$ is a tautology.

No; based on your described context, $(P{\implies}Q)$ likely means that the conditional $(P \to Q)$ is universally true under the assumption of mathematical axioms and definitions, that is, that something like $$\forall x \;\forall y \;\Big(P(x,y) \to Q(x,y)\Big)\tag1$$ is mathematically true. Here, $(P \to Q)$ is not generally a tautology, and, typically, statement $(1)$ is not a logical validity.
In the context of your above sentence, the word always (equivalently: necessarily) is not well-scoped (and actually redundant), and tripping you up: in the current theory, $(P \to Q)$ is (always) true and $Q$ is (always) true whenever $P$ is true.
In short: mathematical truths are generally not tautologies.

$P{\iff}Q$ asserts that $P \leftrightarrow Q$ is a tautology, i.e. $P \leftrightarrow Q$ is always true. $P{\iff}Q$ is also called logical equivalence.

Similarly, based on your described context, $(P{\iff}Q)$ asserts that $P$ and $Q$ are mathematically equivalent, but asserts neither that they are logically nor that they are tautologically equivalent.

Are $\implies$ and $\iff$ just shorthand for saying, "if you start with $P$, you can deduce $Q$" and "if you start with $Q$, you can deduce $P$" etc. ?

Based on your described context, yes (assuming mathematical definitions and results).

I've read that $\implies$ and $\iff$ are not connectives, but that they are making meta statements.

Based on your described context, these two symbols are connectives but not material connectives.

I wasn't aware of the subtle difference in $\to$ and $\implies$.

The following answers that I wrote elaborate on this answer:

*

*material conditional and implication

*material conditional, implication, logical implication

*material biconditional, universal equivalence, equivalence, logical equivalence
