[opentheory-users] necessity of the primitive inference rules

[Ramana Kumar]

Are the OpenTheory inference rules (virtual machine commands that
leave theorems on the stack, apart from axiom) all necessary?
More precisely I mean are they any commands for which there are
certain imports and exports such that any article file with those
imports and exports must include the command, and one such article
exists?

I presume this is also a question about HOL Light's kernel, since
OpenTheory's inference rules are the same... right?