One direction of sb5 is provable from fewer axioms

[wlammen]

1. One direction of sb5 is provable from axioms up to ax-7 only. Add this theorem as sb1v, matching the similar sb1 in name.
2. Delete outdated OLD theorems

[benjub]

I think wl-sb1v should be moved to Main. Can it be used in other theorems (possibly adapting the proofs), in particularly the ones using sb1/sb5 ?

[wlammen]

Can it be used in other theorems (possibly adapting the proofs), in particularly the ones using sb1/sb5 ?

I did a quick check to see whether it helps in other theorems, but I found no instance.

[benjub]

Can it be used in other theorems (possibly adapting the proofs), in particularly the ones using sb1/sb5 ?

I did a quick check to see whether it helps in other theorems, but I found no instance.

To me, even without applications, it's worth it in its own sake. So, now or in a future PR, as you prefer.