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

Detailed syntax breakdown

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