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