Theorem bj-bijust00

Description: A self-implication does not imply the negation of a self-implication. Most general theorem of which bijust is an instance ( bijust0 and bj-bijust0ALT are therefore also instances of it). (Contributed by BJ, 7-Sep-2022)

	Ref	Expression
Assertion	bj-bijust00	⊢ ¬ ( ( 𝜑 → 𝜑 ) → ¬ ( 𝜓 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝜑 → 𝜑 )
2		id	⊢ ( 𝜓 → 𝜓 )
3		pm3.2im	⊢ ( ( 𝜑 → 𝜑 ) → ( ( 𝜓 → 𝜓 ) → ¬ ( ( 𝜑 → 𝜑 ) → ¬ ( 𝜓 → 𝜓 ) ) ) )
4	1 2 3	mp2	⊢ ¬ ( ( 𝜑 → 𝜑 ) → ¬ ( 𝜓 → 𝜓 ) )