Theorem bj-nimn 31721

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 22 and jc 158, however, the present proof uses theorems that are more basic than jc 158. (Proof modification is discouraged.)

Assertion

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

Proof of Theorem bj-nimn

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  bj-nimni  31722