Nearby theorems
|
|
Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-frege31 | Structured version Visualization version Unicode version | ||
Description:  cannot be denied and (at the same time
)  affirmed.
Duplex negatio affirmat. The denial of the denial is affirmation.
Identical to notnotr 125. Axiom 31 of [Frege1879] p. 44. (Contributed by
RP, 24-Dec-2019.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax-frege31 |
 
  |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . . 4
 | |
| 2 | 1 | wn 3 |
. . 3
|
| 3 | 2 | wn 3 |
. 2
|
| 4 | 3, 1 | wi 4 |
1
|
| Colors of variables: wff setvar class |
| This axiom is referenced by: frege32 38129 |
| Copyright terms: Public domain | W3C validator |