Theorem anifp

The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor. (Contributed by BJ, 30-Sep-2019.)

Conclusion
\( \vdash \psi \wedge \chi \rightarrow \operatorname{if} ( \varphi , \psi , \chi ) \)
Proof
l0
olc
olc
l2
anim12i l0 _
\( \vdash \psi \wedge \chi \rightarrow (\neg \varphi \vee \psi) \wedge (\varphi \vee \chi) \)
dfifp4
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\neg \varphi \vee \psi) \wedge (\varphi \vee \chi) \)
sylibr l2 _