Theorem dfifp7

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

Conclusion
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\chi \rightarrow \varphi) \rightarrow \varphi \wedge \psi \)
Proof
l0
orcom
\( \vdash \varphi \wedge \psi \vee \neg (\chi \rightarrow \varphi) \leftrightarrow \neg (\chi \rightarrow \varphi) \vee \varphi \wedge \psi \)
l1
dfifp6
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \neg (\chi \rightarrow \varphi) \)
imor
\( \vdash (\chi \rightarrow \varphi) \rightarrow \varphi \wedge \psi \leftrightarrow \neg (\chi \rightarrow \varphi) \vee \varphi \wedge \psi \)
3bitr4i l0 l1 _