Theorem dfifp5

Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.)

Conclusion
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\neg \varphi \vee \psi) \wedge (\neg \varphi \rightarrow \chi) \)
Proof
l0
dfifp2
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \)
imor
\( \vdash \varphi \rightarrow \psi \leftrightarrow \neg \varphi \vee \psi \)
bianbi l0 _