Consider the FOL of standard set theory.
In any FOL expression in its most formal form, we have four types of objects
$$\color{blue}{\forall} \color{green}{x}(\color{blue}{\exists} \color{green}{y} (\color{green}{x}\in \color{green}{y})\color{red}{\wedge}(\color{green}{y}\color{purple}{\notin}\color{green}{x}))$$
$\color{blue}{\text{Quantifiers}}:$ $\forall$ and $\exists$
$\color{green}{\text{Variables}}:$ $a,b,c,\dots,w,w_0,w_1,\dots$
$\color{red}{\text{Operations}}:$ $\neg,\implies,\iff,\wedge$ and $\vee$
$\color{purple}{\text{Atoms}}:$ $w_0\in w_1$ or $w_0\notin w_1$
Operation Minimization:
If we were trying to minimize this system, we can opt out from having any operations besides the negation $\neg$ and some operation acting as a universal operator, such as $\implies$. I.e, we can define all other binary operations in terms of $\neg$ and $\implies$.
For example, we can simply define $p\vee q\equiv p\implies\neg q$, as these have classically equivalent truth tables.
Atom Minimization:
Furthermore, since $\in$ and $\notin$ are the only atomic relationships between variables in set theory (discounting $\subseteq$, as that can be defined in terms of $\in$), we can define $w_0 \notin w_1$ as $\neg(w_0\in w_1)$.
Variable Minimization:
The amount of variable symbols is countably infinite, and thus cannot be minimized (not that they need to be).
Quantifier minimization:
Since $\forall w_0(\phi(x))\iff \neg(\exists w_0(\neg(\phi(x))))$ for any formula $\phi$, we can define one of the quantifiers in terms of the other. Without loss of generality, let's keep $\forall$ and define $$\exists w_0(\phi(x))\equiv \neg(\forall w_0(\neg(\phi(x)))).$$
Finally, we are left with a logic only in terms of a countable set of variables, one quantifier $\forall$, one unary operation $\neg$, one binary operation $\implies$, and one atomic variable relationship $\in$. But we are not quite done minimizing!
Law minimization:
Syntax alone doesn't suffice for a formal system! We need to define the laws/axioms/transformation rules.
This list on Wikipedia shows that the underlying zero'th order logic has dozens of laws alone. However, many can be deduced from prior ones.
For example, Conjunction, Double Negation, and De Morgan's Theorem suffice to deduce Addition.
Of course, we also must define the first order laws too, such as
$$\forall w_0(\phi(w_0)),\forall w_0(\psi(w_0))\vdash \forall w_0(\phi(w_0)\wedge\psi(w_0))$$
So my question is,
What is the minimal amount of FOL laws required to deduce the rest of the classical laws?
Any insight would be greatly apreciated.