This section gathers theorems of propositional calculus which use (either in
their statement or proof) mixed connectives (at least conjunction and
disjunction).
As noted in the "note on definitions" in the section comment for logical
equivalence, some theorem statements may contain for instance only
conjunction or only disjunction, but both definitions are used in their
proofs to make them shorter (this is exemplified in orim12d versus
orim12dALT). These theorems are mostly grouped at the beginning of this
section.
The family of theorems starting with animorl focus on the relation between
conjunction and disjunction and can be seen as the starting point of mixed
connectives in statements. This sectioning is not rigorously true, since for
instance the section begins with jaao and related theorems.