Minimize ax-13 usage

[GinoGiotto]

Part of https://groups.google.com/g/metamath/c/OB2_9sYgDfA.

Now it comes the truly systematic phase: reducing ax-13 usage with the minimizer.

Each PR will be the result of the scan of 50 theorems, so at most you'll see 50 changed proofs per PR.

I created a new branch named "all", containing the combination of future minimizations. In the "all" branch ax-13 is used by only 3517 proofs (currently ax-13 is used by 25,000 proofs). It is not as good as ax-13-complete, but we shouldn't worry too much about it, because once ax-13 usage will be low it will be easier to identify the "missing chains" to bring that number even lower.

Each change obeys the following criteria:

• A change must drop ax-13 from the theorem whose proof is edited. If a proof is edited without its dependency on ax-13 reduced, then it's either the result of a recompression (so a shortening) or a mistake (I've never seen it so far).

• A change replaces the use of a theorem with its version with more dv, so the general proof length and shape will stay the same.

This PR drops ax-13 from 61 theorems. Full axiom usage here: f489ed8