>>12520776Most answer around here are retarded. They invoke issues about incompleteness by parroting Gödelian speak, but this is totally unrelated to OP's question.
What OP is asking for is called "cut elimination", which is a property that most sane logical systems enjoy. Even so, you can always tweak the definition of your system to make cut elimination hold.
If you express the derivation rules of your system as a programming language à la Curry-Howard, even if it's based on classical logic, you can easily write a normalization procedure that performs full cut elimination, and as such, removes the use of all intermediate theorems. It's very easy to do, but doing it efficiently is harder (see e.g. normalization by evaluation) and in practice most of the time the normalized proofs will be so big that it will take eons before the normalization procedure terminates.
TL;DR: YES. And other posters are retarded faggots.
