This section defines disjunction of two formulas, denoted by infix "" and read "or". It is defined in terms of implication and negation, which is possible in classical logic (but not in intuitionistic logic: see iset.mm). This section contains only theorems proved without df-an (theorems that are proved using df-an are deferred to the next section). Basic theorems that help simplifying and applying disjunction are olc, orc, and orcom.
As mentioned in the "note on definitions" in the section comment for logical equivalence, all theorems in this and the previous section can be stated in terms of implication and negation only. Additionally, in classical logic (but not in intuitionistic logic: see iset.mm), it is also possible to translate conjunction into disjunction and conversely via the De Morgan law anor: conjunction and disjunction are dual connectives. Either is sufficient to develop all propositional calculus of the logic (together with implication and negation). In practice, conjunction is more efficient, its big advantage being the possibility to use it to group antecedents in a convenient way, using imp and ex as noted in the previous section.
An illustration of the conservativity of df-an is given by orim12dALT, which is an alternate proof of orim12d not using df-an.