Theorem bj-nnim 13616

Description: The double negation of an implication implies the implication with the consequent doubly negated. (Contributed by BJ, 24-Nov-2023.)

Assertion

Ref	Expression
bj-nnim	⊢ (¬ ¬ (𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))

Proof of Theorem bj-nnim

Step	Hyp	Ref	Expression
1		jcn 641	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓)))
2	1	con3rr3 623	1 ⊢ (¬ ¬ (𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 604  ax-in2 605

This theorem is referenced by:  bj-stim  13627