Axiom ax-frege31 43847

Description: 𝜑 cannot be denied and (at the same time ) ¬ ¬ 𝜑 affirmed. Duplex negatio affirmat. The denial of the denial is affirmation. Identical to notnotr 130. 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

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2	1	wn 3	. . 3 wff ¬ 𝜑
3	2	wn 3	. 2 wff ¬ ¬ 𝜑
4	3, 1	wi 4	1 wff (¬ ¬ 𝜑 → 𝜑)

This axiom is referenced by:  frege32  43848