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)
|- -. -. ph
|- ph
|- ( -. ph -> -. -. -. ph )