What's the difference between $\equiv$ and $\leftrightarrow$ in a formal proof? Some texts and online sources seem to imply that they're interchangeable, while others say that there is at least a small nuanced difference between the two.
For example, I've read that $ \equiv $ can be read as "can be replaced in a logical proof with...", yet I've also seen $ \leftrightarrow $ used in that same vein.
Edit:
I'm trying to write my own textbook on this material as a way of forcing me to learn as much as possible before my final in 3 weeks. I'm trying to figure out a way to describe what $ \equiv $ means, while I've described $ \leftrightarrow $ as "If and only if"
 A: With respect to the "$\equiv$" symbol (my comment was getting long!):
This is more in the way of speculation, but it seems that "$a \equiv b$" is used in some (not all) contexts to denote "$a$ is identically $b$", or in other contexts to convey that $a$ and $b$ are essentially equivalent (with respect to some equivalence-relation, e.g. congruence modulo $n$, or geometric congruence, or truth-functionality, or... etc.), again, depending on the contexts in which it's being used. 
This would be consistent with the frequent use of the symbol "$\equiv$" in introductory logic texts to convey that $a \equiv b$ holds (is true) whenever $a$ and $b$ evaluate to the same truth value. It's also consistent with what you've read:  "$\equiv$" can be read as "can be replaced in a logical proof with...", in the sense that if "$p\equiv q$", then replacing every occurrence of $p$ with $q$ (or vice-versa) will not change the truth-value of any propositions thus impacted. 
I know that I've used "$\equiv$" and "$\leftrightarrow$" interchangeably on this site, when answering, e.g., questions about propositional logic: partly for reasons related to trying to match the notation used in the question, and partly due to being careless and/or not necessarily knowing better.
A: Some author as do use $\equiv$ to mean "if and only if". Another option, which I use from time to time, is to use $\equiv$ as a sort of equality symbol when I am talking about formulas. If I want to give the name $\phi$ to the formula "$a=b"$, I don't want to write
$$
\phi = a = b
$$
so I write
$$
\phi \equiv a = b
$$
instead. This allows me to avoid using quotation symbols.
This latter usage is not documented anywhere, I as far as I know. I am not aware of any book that describes it in detail. But I can explain my motivations for using it:


*

*I don't want to re-use the $=$ sign for another purpose; the first displayed formula is not appealing. But quotation marks in displayed formulas are also unappealing. 

*When I write $\phi \equiv a = b$, I sometimes don't care if $\phi$ is the formula $a=b$ or is just equivalent to it. But for the rest of the proof I will act as if it is that formula. So the $\equiv$ symbol, which connotes "equivalent", suggests that all that matters in the beginning is that $\phi$ is equivalent to $a=b$. 
A: In propositional calculus there is a connective $\rightarrow$ and often one for $\leftrightarrow$, which is a part of the formal language and how we create new propositions; and there is another form, $\implies$ and $\iff$ (also written as $\cong$) which are meta-statements.
Whereas $\varphi\leftrightarrow\psi$ is a proposition, $\varphi\iff\psi$ is a statement about propositions.
It is true, however, that $\varphi\iff\psi$ is true, if and only if $\varphi\leftrightarrow\psi$ is a tautology. However there is a difference between a proposition, and a statement about propositions; and I cannot stress this difference enough in this post.
A: "$↔$" denotes an equivalent statement in formal logic.
e.g. $A^B ↔ B^A$ (because of the commutative properties).
While "$≡$" denotes an equivalent statement in a mathematical equation, but definition wise it means "identical to".
e.g. $3 \times 4 ≡ 4 \times 3$ (because of the commutative properties).
While like others said these can be interchangeable because they do mean the same thing you usually see "$↔$" in formal logic and "$≡$" in mathematical equations.
I should also note this perspective is from a CS major and may vary from a mathematical majors perspective, but this is what I was taught.
You may want to check Mathematical Structures for Computer Science (2007) by Judith L. Gersting out. It is the book I am currently using for my Discrete Structures class.
