restore the alternative restricted quantifiers in my mathbox (#3268)

* restore the alternative restricted quantifiers in my mathbox

* delete OLD theorems

Author: wlammen

discouraged

@@ -17767,14 +17767,10 @@ New usage of "swrdtrcfv0OLD" is discouraged (1 uses).
 New usage of "swrdtrcfvOLD" is discouraged (2 uses).
 New usage of "swrdtrcfvlOLD" is discouraged (1 uses).
 New usage of "syl2an23anOLD" is discouraged (0 uses).
-New usage of "syl3an2OLD" is discouraged (0 uses).
-New usage of "syl3an3OLD" is discouraged (0 uses).
 New usage of "syl3anl2OLD" is discouraged (0 uses).
 New usage of "syl3anr2OLD" is discouraged (0 uses).
 New usage of "syl5imp" is discouraged (0 uses).
 New usage of "syl5impVD" is discouraged (0 uses).
-New usage of "syld3an1OLD" is discouraged (0 uses).
-New usage of "syld3an2OLD" is discouraged (0 uses).
 New usage of "symdif2OLD" is discouraged (0 uses).
 New usage of "symdifassOLD" is discouraged (0 uses).
 New usage of "tb-ax1" is discouraged (3 uses).
@@ -19639,14 +19635,10 @@ Proof modification of "swrdtrcfv0OLD" is discouraged (95 steps).
 Proof modification of "swrdtrcfvOLD" is discouraged (111 steps).
 Proof modification of "swrdtrcfvlOLD" is discouraged (114 steps).
 Proof modification of "syl2an23anOLD" is discouraged (27 steps).
-Proof modification of "syl3an2OLD" is discouraged (19 steps).
-Proof modification of "syl3an3OLD" is discouraged (18 steps).
 Proof modification of "syl3anl2OLD" is discouraged (24 steps).
 Proof modification of "syl3anr2OLD" is discouraged (23 steps).
 Proof modification of "syl5imp" is discouraged (23 steps).
 Proof modification of "syl5impVD" is discouraged (57 steps).
-Proof modification of "syld3an1OLD" is discouraged (23 steps).
-Proof modification of "syld3an2OLD" is discouraged (23 steps).
 Proof modification of "symdif2OLD" is discouraged (59 steps).
 Proof modification of "symdifassOLD" is discouraged (118 steps).
 Proof modification of "symrefref3" is discouraged (75 steps).