Theorem dfifp4

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

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