Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-frege31 Structured version   Visualization version   GIF version

Axiom ax-frege31 37610
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.)
Assertion
Ref Expression
ax-frege31 (¬ ¬ 𝜑𝜑)

Detailed syntax breakdown of Axiom ax-frege31
StepHypRef Expression
1 wph . . . 4 wff 𝜑
21wn 3 . . 3 wff ¬ 𝜑
32wn 3 . 2 wff ¬ ¬ 𝜑
43, 1wi 4 1 wff (¬ ¬ 𝜑𝜑)
Colors of variables: wff setvar class
This axiom is referenced by:  frege32  37611
  Copyright terms: Public domain W3C validator