Theorem ifpdfbiOLD

Obsolete version of ifpdfbi as of 25-Jun-2026. Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \operatorname{if} ( \varphi , \psi , \neg \psi ) \)
Proof
con34b
l1
anbi2i _
\( \vdash (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \neg \psi) \)
l2
dfbi2
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi) \)
dfifp2
\( \vdash \operatorname{if} ( \varphi , \psi , \neg \psi ) \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \neg \psi) \)
3bitr4i l1 l2 _