Theorem bj-nimn 37188

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

Assertion

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

Proof of Theorem bj-nimn

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  bj-nimni  37189