Theorem ifpid

Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of [ifid]. This is essentially pm4.42. (Contributed by BJ, 20-Sep-2019.)

Conclusion
\( \vdash \operatorname{if} ( \varphi , \psi , \psi ) \leftrightarrow \psi \)
Proof
l0
ifptru
\( \vdash \varphi \rightarrow (\operatorname{if} ( \varphi , \psi , \psi ) \leftrightarrow \psi) \)
ifpfal
\( \vdash \neg \varphi \rightarrow (\operatorname{if} ( \varphi , \psi , \psi ) \leftrightarrow \psi) \)
pm2.61i l0 _