Theorem dfifp6

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

Conclusion
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \neg (\chi \rightarrow \varphi) \)
Proof
l0
df-ifp
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
l1
ancom
\( \vdash \neg \varphi \wedge \chi \leftrightarrow \chi \wedge \neg \varphi \)
annim
\( \vdash \chi \wedge \neg \varphi \leftrightarrow \neg (\chi \rightarrow \varphi) \)
bitri l1 _
orbi2i _
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \chi \leftrightarrow \varphi \wedge \psi \vee \neg (\chi \rightarrow \varphi) \)
bitri l0 _