Theorem wl-luk-notnotr 38200

Description: Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. In classical logic (our logic) this is always true. In intuitionistic logic this is not always true; in intuitionistic logic, when this is true for some 𝜑, then 𝜑 is stable. Copy of notnotr 131 with a different proof. (Contributed by Wolf Lammen, 17-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)

Assertion

Ref	Expression
wl-luk-notnotr	⊢ (¬ ¬ 𝜑 → 𝜑)

Proof of Theorem wl-luk-notnotr

Step	Hyp	Ref	Expression
1		wl-luk-id 38199	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	wl-luk-con1i 38194	1 ⊢ (¬ ¬ 𝜑 → 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-luk1 38175  ax-luk2 38176  ax-luk3 38177

This theorem is used by: (None)