What is the difference between $\leftrightarrow$, $\iff$, and $\equiv$, especially when used in the same text?

Question

I think that the difference has something to do with object language and meta language, but I'm not sure.

I've heard that $\leftrightarrow$ is a connective on a proposition level, whereas $\iff$ is a statement about propositions. But where does $\equiv$ come in?

I've seen texts that use either ($\leftrightarrow$ and $\iff$) or ($\iff$ and $\equiv$). But how do those three relate if they are all used at the same time? Would such use imply that there can be a meta language of a meta language? If not, which pairing makes more sense to use?

Answer 1

↔ short left right arrow - has not default meaning, reference If_and_only_if.

⟺ double short left right arrow - has not default meaning, but can be used in books about List of logic symbols.

≡ congruent - has not default meaning. Look up congruent in the context of modulo division classes. ⟺ double short left right arrow might indicate that too.

For reference purposes look at Operators Without Built-In Meanings. These are symbols available both in LATEX and MathML. In these they have just the names I gave in first place and are entered in a short form. These names are known to google for example, ↔ short left right arrow LATEX or w3.org operator dictionary for MatML as appendix.