 For a taste of what they can do, notice that they yield a succinct justification of a rule of Uniform Substitution, whereby a formula of the form \(A(B/p)\) is a theorem whenever \(A\) is a theorem, provided that \(B\) is free for \(p\) in \(A\). So, for example, if \(p\rightarrow (q \rightarrow p)\) is a theorem, then \(\neg r \rightarrow (q \rightarrow \neg r)\) is likewise a theorem, since this last formula is just \(p\rightarrow (q \rightarrow p)(\neg  r/p)\).[14]