Axiom ax-frege31

Description: ph cannot be denied and (at the same time ) -. -. ph affirmed. Duplex negatio affirmat. The denial of the denial is affirmation. Identical to notnotr . Axiom 31 of Frege1879 p. 44. (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-frege31	$$⊢\neg \neg \phi \to \phi$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1	0	wn	$$wff\neg \phi$$
2	1	wn	$$wff\neg \neg \phi$$
3	2 0	wi	$$wff\left(\neg \neg \phi \to \phi \right)$$