Theorem casesifp

Version of cases expressed using if-. Case disjunction according to the value of \( \varphi \). One can see this as a proof that the two hypotheses characterize the conditional operator for propositions. For the converses, see ifptru and ifpfal. (Contributed by BJ, 20-Sep-2019.)

Hypotheses
casesifp.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
casesifp.2
\( \vdash \neg \varphi \rightarrow (\psi \leftrightarrow \theta) \)
Conclusion
\( \vdash \psi \leftrightarrow \operatorname{if} ( \varphi , \chi , \theta ) \)
Proof
l0
casesifp.1
casesifp.2
l2
cases l0 _
\( \vdash \psi \leftrightarrow \varphi \wedge \chi \vee \neg \varphi \wedge \theta \)
df-ifp
\( \vdash \operatorname{if} ( \varphi , \chi , \theta ) \leftrightarrow \varphi \wedge \chi \vee \neg \varphi \wedge \theta \)
bitr4i l2 _