Theorem ifptru

Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of [iftrue]. This is essentially dedlema. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)

Conclusion
\( \vdash \varphi \rightarrow (\operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow \psi) \)
Proof
l0
biimt
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \varphi \rightarrow \psi) \)
orc
l2
biantrud _
\( \vdash \varphi \rightarrow (\varphi \rightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\varphi \vee \chi)) \)
dfifp3
\( \vdash \operatorname{if} ( \varphi , \psi , \chi ) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\varphi \vee \chi) \)
bitr4di l2 _
\( \vdash \varphi \rightarrow (\varphi \rightarrow \psi \leftrightarrow \operatorname{if} ( \varphi , \psi , \chi )) \)
bitr2d l0 _