Theorem notnotri 132

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

Hypothesis

Ref	Expression
notnotri.1	⊢ ¬ ¬ 𝜑

Assertion

Ref	Expression
notnotri	⊢ 𝜑

Proof of Theorem notnotri

Step	Hyp	Ref	Expression
1		notnotri.1	. 2 ⊢ ¬ ¬ 𝜑
2	1	pm2.21i 120	. 2 ⊢ (¬ 𝜑 → ¬ ¬ ¬ 𝜑)
3	1, 2	mt4 117	1 ⊢ 𝜑

This proof depends on syntax axioms:  ¬ wn 3

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-3 8

This theorem is used by:  mt3  204  antnest  36220  pm2.65ni  45826