Consider the category of strings over some alphabet $\Sigma$, where each string is a reasonable representation (in some human language) of a proposition that has been proven true, or is axiomatized to be true, or thirdly is asserted to be true in preparation for a proof. For example you might see "Let $G$ be a group." as a string, but then there's also "Let $H$ be a group." and so on. I'm looking at this from a string parsing perspective, is why.
Anyway, draw an arrow between any two strings such that one implies the other (in whatever chosen language). If $A \implies B$ then there is an arrow from $A$ to $B$ in the category, where $A, B$ are strings.
This is indeed a category, correct?
Reason is because all the statement strings are assumed to be true.
If you handle all the details correctly, then yes, constructions like this produce categories (more specifically preorders), basically because implication is transitive ("hypothetical syllogism"): if $A \Rightarrow B$ and $B \Rightarrow C$ then $A \Rightarrow C$.
There's some work to do in handling all the details correctly. As in the comments, depending on exactly what kind of statements you're working with you may end up with a very small category (up to equivalence), which may only have one isomorphism class of object (all the true statements) or two isomorphism classes of objects (all the true statements, all the false statements). For more interesting variations see, for example, Heyting algebra and this blog post.
Here's one possible variation which sounds like it's along the lines of what you want. Choose a first-order theory $T$, say Peano arithmetic or the theory of groups, and consider the collection $F_T$ all well-formed formulas in that theory. For Peano arithmetic this will be statements like "for all positive integers $a, b$, it's the case that $a + b = b + a$" and for group theory this will be statements like "for all elements $g$ it's the case that $g \cdot g^{-1} = g^{-1} \cdot g = e$" ($g$ belongs to an implicit background group $G$).
$F_T$ forms quite an interesting preorder under implication in general. There are at least two isomorphism classes of objects, namely the provably true and the provably false statements, which are precisely the statements true resp. false in all models of the theory $T$ (by the completeness theorem). But in general there may be statements in $F_T$ which are neither provably true nor provably false, which (again by the completeness theorem) are precisely the statements which are true in some models but false in others. For Peano arithmetic such statements exist by the incompleteness theorems, and for groups one can very explicitly exhibit examples such as "$\forall g, g^2 = e$." These statements can have interesting implication relations with each other, which are reflected in the embedding of $F_T$ into the poset of subsets of the set of models of $T$ given by sending a statement in $F_T$ to the set of all models in which it's true. (Strictly speaking, the collection of models of $T$ may be too large to form a set, so I should say "subclass of the class of all models..." or something awkward like that.)