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	|- ( ( ph <-> ( ph <-> ps ) ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		biid	|- ( ph <-> ph )
2		biass	|- ( ( ( ph <-> ph ) <-> ps ) <-> ( ph <-> ( ph <-> ps ) ) )
3	2	biimpri	|- ( ( ph <-> ( ph <-> ps ) ) -> ( ( ph <-> ph ) <-> ps ) )
4	1 3	mpbii	|- ( ( ph <-> ( ph <-> ps ) ) -> ps )