Theorem bj-nimn

Description: If a formula is true, then it does not imply its negation. (Contributed by BJ, 19-Mar-2020) A shorter proof is possible using id and jc , however, the present proof uses theorems that are more basic than jc . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nimn	⊢ ( 𝜑 → ¬ ( 𝜑 → ¬ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.01	⊢ ( ( 𝜑 → ¬ 𝜑 ) → ¬ 𝜑 )
2	1	con2i	⊢ ( 𝜑 → ¬ ( 𝜑 → ¬ 𝜑 ) )