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

Proof

Step	Hyp	Ref	Expression
1		pm2.01	|- ( ( ph -> -. ph ) -> -. ph )
2	1	con2i	|- ( ph -> -. ( ph -> -. ph ) )