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	|- ( ph -> -. -. ph )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1	0	wn	|- -. ph
2	1	wn	|- -. -. ph
3	0 2	wi	|- ( ph -> -. -. ph )