Nearby theorems
|
|
Mathbox for Jim Kingdon |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > Mathboxes > nnnotnotr | Unicode version | ||
| Description: Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 840, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.) |
| Ref | Expression |
|---|---|
| nnnotnotr |
  
   |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | conax1 643 |
. 2
| |
| 2 | pm2.24 611 |
. . 3
| |
| 3 | 2 | con3i 622 |
. 2
|
| 4 | 1, 3 | pm2.65i 629 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 3
wi 4 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 604 ax-in2 605 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |