Alternate definition of the conditional operator for propositions. The
value of \( \operatorname{if} ( \varphi , \psi , \chi ) \) is "if \( \varphi \) then \( \psi \), and if not
\( \varphi \) then \( \chi \) ". This is the definition used in Section II.24 of
[Church] p. 129 (Definition D12 page 132) (see comment of [df-ifp] ).
(Contributed by BJ, 22-Jun-2019.)
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \)
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \chi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \)