Table of Contents - 1.2.9. The conditional operator for propositions
This subsection introduces the conditional operator for propositions, denoted
by (see df-ifp). It is the analogue for
propositions of the conditional operator for classes, denoted by
(see df-if).