Theorem ifpor

The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp. (Contributed by BJ, 1-Oct-2019.)

Conclusion
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \rightarrow \psi \vee \chi \)
Proof
l0
df-ifp
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
l1
simpr
simpr
orim12i l1 _
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \chi \rightarrow \psi \vee \chi \)
sylbi l0 _