jsalvatier:

I didn't mean to say that you couldn't use what you had derived later on, but if you can define a theory with with 1 operator, why do it with more?

Because it's far easier to work that way. You don't need ten different digits to work with natural numbers either, but we still do it for convenience. When you see the formula (p&q)->r, it's much easier to figure out what's going on than if it's in the form ((p|q)|(p|q))|(r|r). (Here "|" is the Sheffer symbol, i.e. NAND, which is by itself functionally complete.)

Is there a formal concept of an alias in math (for example, "a implies b" could be an alias for "(not a) or b")?

Math texts often introduce some notational aliases to make the text more readable, and logic texts do it almost invariably. For example, in the standard syntax of first-order logic, "+" is a binary function symbol, and "=" is a binary predicate, but it's still customary to introduce easier to read notation "x+y" and "x=y" where it should be "+xy" and "=xy". However, these conventions don't have any implications for the actual results being proven and discussed; the theorems still talk about formulas containing "+xy", and you just translate on the fly between that notation and the intuitive one as necessary.

In contrast, introducing additional operators into your definition of logic formulas changes things significantly, since now all your proofs have to account for these additional sorts of well-formed formulas, and also the formal proof system you use must be able to handle them. On the other hand, a good choice of a non-minimal functionally complete set of operators will make the entire work much easier to handle. So in practice, a non-minimal set is normally used. You can also use notation conventions like p->q instead of (~p v q) as long as their relations with the formal syntax are clear and simple enough. (Which definitely wouldn't be the case if you based the entire logic on just NAND and then tried to define AND, OR, etc. as notational aliases.)