Theorem ifpdfbi

Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.) (Proof shortened by Garrett Katz, 25-Jun-2026.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \operatorname{if} ( \varphi , \psi , \neg \psi ) \)
Proof
l0
dfbi3
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \neg \psi \)
df-ifp
\( \vdash \operatorname{if} ( \varphi , \psi , \neg \psi ) \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \neg \psi \)
bitr4i l0 _