Theorem dfifp3

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

Conclusion
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\varphi \vee \chi) \)
Proof
l0
dfifp2
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \)
pm4.64
anbi2i _
\( \vdash (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\varphi \vee \chi) \)
bitri l0 _