This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem notnoti

Description: Inference associated with notnot . (Contributed by NM, 27-Feb-2008)

Ref Expression
Hypothesis notnoti.1 ⊢ 𝜑
Assertion notnoti ¬ ¬ 𝜑

Proof

Step Hyp Ref Expression
1 notnoti.1 ⊢ 𝜑
2 notnot ⊢ ( 𝜑 → ¬ ¬ 𝜑 )
3 1 2 ax-mp ⊢ ¬ ¬ 𝜑