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

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 
|- -. -. ph
Assertion notnotri 
|- ph

Proof

Step Hyp Ref Expression
1 notnotri.1 
 |-  -. -. ph
2 1 pm2.21i 
 |-  ( -. ph -> -. -. -. ph )
3 1 2 mt4 
 |-  ph