Theorem ifpfal

Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of [iffalse]. This is essentially dedlemb. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.)

Conclusion
\( \vdash \neg \varphi \rightarrow (\operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \chi) \)
Proof
l0
ifpn
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \operatorname{if} ( \neg \varphi , \chi , \psi ) \)
ifptru
\( \vdash \neg \varphi \rightarrow (\operatorname{if} ( \neg \varphi , \chi , \psi ) \leftrightarrow \chi) \)
bitrid l0 _