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	$$⊢\phi \to \neg \left(\phi \to \neg \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		pm2.01	$$⊢\left(\phi \to \neg \phi \right)\to \neg \phi$$
2	1	con2i	$$⊢\phi \to \neg \left(\phi \to \neg \phi \right)$$