Axiom ax-frege41

Description: The affirmation of ph denies the denial of ph . Identical to notnot . Axiom 41 of Frege1879 p. 47. (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-frege41	$$⊢\phi \to \neg \neg \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	0 2	wi	$$wff\left(\phi \to \neg \neg \phi \right)$$