Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-nimn Structured version   Visualization version   GIF version

Theorem bj-nimn 33796
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 164, however, the present proof uses theorems that are more basic than jc 164. (Proof modification is discouraged.)
Assertion
Ref Expression
bj-nimn (𝜑 → ¬ (𝜑 → ¬ 𝜑))

Proof of Theorem bj-nimn
StepHypRef Expression
1 pm2.01 190 . 2 ((𝜑 → ¬ 𝜑) → ¬ 𝜑)
21con2i 141 1 (𝜑 → ¬ (𝜑 → ¬ 𝜑))
Colors of variables: wff setvar class
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  33797
  Copyright terms: Public domain W3C validator