Theorem ifpn

Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) (Proof shortened by Wolf Lammen, 5-May-2024.)

Conclusion
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \operatorname{if} ( \neg \varphi , \chi , \psi ) \)
Proof
l0
ancom
\( \vdash (\neg \varphi \vee \psi) \wedge (\neg \varphi \rightarrow \chi) \leftrightarrow (\neg \varphi \rightarrow \chi) \wedge (\neg \varphi \vee \psi) \)
l1
dfifp5
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\neg \varphi \vee \psi) \wedge (\neg \varphi \rightarrow \chi) \)
dfifp3
\( \vdash \operatorname{if} ( \neg \varphi , \chi , \psi ) \leftrightarrow (\neg \varphi \rightarrow \chi) \wedge (\neg \varphi \vee \psi) \)
3bitr4i l0 l1 _