Metamath Proof Explorer


Theorem notnotri

Description: Inference associated with notnotr . For a shorter proof using ax-2 , see notnotriALT . (Contributed by NM, 27-Feb-2008) (Proof shortened by Wolf Lammen, 15-Jul-2021) Remove dependency on ax-2 . (Revised by Steven Nguyen, 27-Dec-2022)

Ref Expression
Hypothesis notnotri.1 ¬ ¬ φ
Assertion notnotri φ

Proof

Step Hyp Ref Expression
1 notnotri.1 ¬ ¬ φ
2 1 pm2.21i ¬ φ ¬ ¬ ¬ φ
3 1 2 mt4 φ