# Metamath Proof Explorer

This section defines conjunction of two formulas, denoted by infix "" and read "and". It is defined in terms of implication and negation, which is possible in classical logic (but not in intuitionistic logic: see iset.mm).

After the definition, we briefly introduce conversion of simple expressions to and from conjunction. Two simple operations called importation (imp) and exportation (ex) follow. In the propositions-as-types interpretation, they correspond to uncurrying and currying respectively. They are foundational for this section. Most of the theorems proved here trace back to them, mostly indirectly, in a layered fashion, where more complex expressions are built from simpler ones. Here are some of these successive layers: importation and exportation, commutativity and associativity laws, adding antecedents and simplifying, conjunction of consequents, syllogisms, etc.

As indicated in the "note on definitions" in the section comment for logical equivalence, some theorems containing only implication, negation and conjunction are placed in the section after disjunction since theirs proofs use disjunction (although this is not required since definitions are conservative, see said section comment).