The last time I was into formal languages for proofs, (first order logic) I concluded that modus ponens and verification of instances of a few simple axiom schema suffice theoretically, but with possible exponential blowup. This is very close to definition of a proof. Allowing the same verification logic to do substitutions on proven propositions is sound and makes the proof checking program scarcely bigger and I think avoids the exponential blowup. This is because with the extended rules you can build a collection of theorems for reuse.