In a base for propositional logic using the Polish connective $\uparrow$ for not both, J. Nicod isolated one axiom as sufficient:

$\uparrow\uparrow p\uparrow q r\uparrow\uparrow t\uparrow tt\uparrow\uparrow s q\uparrow\uparrow p s\uparrow ps$

J. Nicod used the somewhat odd inference rule $r$ if $\uparrow p\uparrow q r$ and $p$. May we use $\uparrow p\uparrow p r$ and $p$ instead of Nicod's rule, or is there some deeper reason for using $q$?