Theorem currybi

Description: Biconditional version of Curry's paradox. If some proposition ph amounts to the self-referential statement "This very statement is equivalent to ps ", then ps is true. See bj-currypara in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025)

	Ref	Expression
Assertion	currybi	$$⊢\left(\phi \leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)\to \psi$$

Proof

Step	Hyp	Ref	Expression
1		biid	$$⊢\phi \leftrightarrow \phi$$
2		biass	$$⊢\left(\left(\phi \leftrightarrow \phi \right)\leftrightarrow \psi \right)\leftrightarrow \left(\phi \leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)$$
3	2	biimpri	$$⊢\left(\phi \leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)\to \left(\left(\phi \leftrightarrow \phi \right)\leftrightarrow \psi \right)$$
4	1 3	mpbii	$$⊢\left(\phi \leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)\to \psi$$