Axiom ax-frege41 41453

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

Assertion

Ref	Expression
ax-frege41	⊢ (𝜑 → ¬ ¬ 𝜑)

Detailed syntax breakdown of Axiom ax-frege41

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

This axiom is referenced by:  frege42  41454