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	⊢ ( ( 𝜑 ↔ ( 𝜑 ↔ 𝜓 ) ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		biid	⊢ ( 𝜑 ↔ 𝜑 )
2		biass	⊢ ( ( ( 𝜑 ↔ 𝜑 ) ↔ 𝜓 ) ↔ ( 𝜑 ↔ ( 𝜑 ↔ 𝜓 ) ) )
3	2	biimpri	⊢ ( ( 𝜑 ↔ ( 𝜑 ↔ 𝜓 ) ) → ( ( 𝜑 ↔ 𝜑 ) ↔ 𝜓 ) )
4	1 3	mpbii	⊢ ( ( 𝜑 ↔ ( 𝜑 ↔ 𝜓 ) ) → 𝜓 )