Biconditional

In logic and mathematics, the logical biconditional (sometimes known as the material biconditional) is the logical connective of two statements asserting "p if and only if q", where p is an antecedent and q is a consequent. This is often abbreviated "p iff q". The operator is denoted using a doubleheaded arrow (↔), a prefixed E (Epq), an equality sign (=), an equivalence sign (≡), or EQV. It is logically equivalent to (p → q) ∧ (q → p), or the XNOR (exclusive nor) boolean operator. It is equivalent to "(not p or q) and (not q or p)". It is also logically equivalent to "(p and q) or (not p and not q)", meaning "both or neither".

The only difference from material conditional is the case when the hypothesis is false but the conclusion is true. In that case, in the conditional, the result is true, yet in the biconditional the result is false.

In the conceptual interpretation, a = b means "All a 's are b 's and all b 's are a 's"; in other words, the sets a and b coincide: they are identical. This does not mean that the concepts have the same meaning. Examples: "triangle" and "trilateral", "equiangular trilateral" and "equilateral triangle". The antecedent is the subject and the consequent is the predicate of a universal affirmative proposition.

In the propositional interpretation, a ⇔ b means that a implies b and b implies a; in other words, that the propositions are equivalent, that is to say, either true or false at the same time. This does not mean that they have the same meaning. Example: "The triangle ABC has two equal sides", and "The triangle ABC has two equal angles". The antecedent is the premise or the cause and the consequent is the consequence. When an implication is translated by a hypothetical (or conditional) judgment the antecedent is called the hypothesis (or the condition) and the consequent is called the thesis.

A common way of demonstrating a biconditional is to use its equivalence to the conjunction of two converse conditionals, demonstrating these separately.

...
Wikipedia