Theorem wl-luk-notnotr 35521

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 132 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 35520	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	wl-luk-con1i 35515	1 ⊢ (¬ ¬ 𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-luk1 35496  ax-luk2 35497  ax-luk3 35498

This theorem is referenced by: (None)