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	⊢ ( 𝜑 → ¬ ¬ 𝜑 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1	0	wn	⊢ ¬ 𝜑
2	1	wn	⊢ ¬ ¬ 𝜑
3	0 2	wi	⊢ ( 𝜑 → ¬ ¬ 𝜑 )