Levon's answer settles the question whether the claims "$A\rightarrow A$ is provable" and "$A\leftrightarrow A$ is provable" are themselves provable.
Whether they are true (independent of being provable) is a different matter.
Let $M$ bet whatever foundation of mathematics we choose to work with. Gödel's incompleteness theorem tells us that $A\Rightarrow (M\vdash A)$ cannot be not true in general for interesting $M$'s. Thus $(M\vdash A)\Leftrightarrow A$ must be rejected.
On the other hand, we should very much hope that $(M\vdash A) \Rightarrow A$ is a Platonically true statement -- that is, we only want true statements to be provable. If that doesn't hold, then either the logic implicit in the $\vdash$ symbol is flawed, or the axioms of $M$ are not true.
Gödel and Rosser tell us that we cannot establish $(M\vdash A)\Rightarrow A$ this by purely formal means, but most mathematicians manage to somehow convince themselves informally or intuitively. If not, they either become formalists or leave the field.
As for $B\lor \neg B$, this is indeed always a theorem in mainstream mathematical logic, so-called "classical logic".
About a century ago, there was a movement called "the intuitionists" who rejected this and favored a more restricted mode of mathematical reasoning where $B\lor \neg B$ was not always a theorem. There are very few today who seriously think mathematics in general should be so restricted, though it is not uncommon to investigate the restricted intuitionistic logic as an object of study rather than as a foundation of mathematics. Viewed this way it turns out to have some interesting applications in, e.g., computer science.