### IFF

logical ``if and only if''
Major Section: ACL2-BUILT-INS

`Iff`

is the ACL2 biconditional, ``if and only if''. `(iff P Q)`

means that either `P`

and `Q`

are both false (i.e., `nil`

) or both true
(i.e., not `nil`

).

To see the ACL2 definition of this function, see pf.