Iff: In logic: Term for if and only if, equivalence, bi-implication.

The term 'iff' or 'if and only if' is a logical term. In English, it is usually rendered with four words, and one reason to prefer 'iff' over 'if and only if' is that it is one word. It is used to convey that the two statements it connects, as in 'p iff q' are such that the each follows from the other, in the sense that if one has derived p and also has derived that p iff q, that then one may infer q, and also that if one has derived q and also has derived that p iff q, that then one may infer p.

In formal logic, 'if and only if' is often written as 'iff' or as '3' or as '<=>' and rules that are adopted for 'iff' are often these:

From (p iff q) it follows that (p --> q).
From (p iff q) it follows that (q --> p).
From (p --> q) and (q --> p) it follows that (p iff q).

That is: If p iff q is true, then so are p implies q and q implies p, and conversely if both p implies q and q implies p are true then p iff q is true. The table for p iff q is:

This shows that 'iff' can be wholly avoided, though usually it isn't because it is quite handy to have a brief expression for the statement of logical equivalence.

Note that (p iff q) as defined by the table amounts to ((p&q) V (~p&~q)), which is to say that (p iff q) precisely if either both p and q or both not-p and not-q, which again amounts to: Both are true or both are not true, or again: both have the same truth-value.

This definition also makes it possible to use ~(p iff q) as an expression for exclusive disjunction, since it amounts to: Either p is true and q is not true or p is not true and q is true.

Some theorems in Propositional Logic concerning iff:

T1. (p iff p)
T2. (p iff q) iff (q iff p)
T3. ((p iff q) & (q iff r)) --> (p iff r)
T4. (p iff q) iff (~p iff ~q)
T5. (~(p iff q)) iff (p iff ~q)
T6. (p iff ~q) iff (~p iff q)