Theorem ifpimpda

Separation of the values of the conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 27-Feb-2021.)

Hypotheses
ifpimpda.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
ifpimpda.2
\( \vdash \varphi \wedge \neg \psi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \operatorname{if} ( \psi , \chi , \theta ) \)
Proof
ifpimpda.1
l1
ex _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
ifpimpda.2
l3
ex _
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \theta \)
dfifp2
\( \vdash \operatorname{if} ( \psi , \chi , \theta ) \leftrightarrow (\psi \rightarrow \chi) \wedge (\neg \psi \rightarrow \theta) \)
sylanbrc l1 l3 _