Foundation·F05
Conjunction
A and B: prove both to assert it, recover each from it.
To prove a conjunction, prove both conjuncts; from a conjunction, extract either conjunct.
Part of the logical framework beneath ZFC (classical first-order logic with equality): taken as given rather than proven, it belongs to the language the set-theoretic axioms are stated in.
Remarks
The three rules fix the meaning of
completely (see the logical framework): a proof of
carries exactly the information of a proof of
paired with a proof of
. Classically
is definable from other connectives, for instance
as
, but no such basis is canonical, and the rules match how conjunction is actually used. In Lean, And is a structure whose constructor And.intro is the introduction rule and whose projections .left and .right are the two eliminations.
Used by
Propose an edit4 published revisions
- 7/12/2026 · Benjamin· Remove the In words reading and its highlight markup: this article states three inference rules, not a single formula with a natural plain-English translation.what changed →
- 7/12/2026 · Benjamin· Rewrite the In words reading to cover both the introduction and the two elimination rules.what changed →
- 7/11/2026 · Benjamin· Fix Mathlib link: add the #doc fragment doc-gen4's find endpoint requires (old link 404'd). Content unchanged.what changed →
- 7/11/2026 · Benjamin· Logic layer: connectives and quantifierswhat changed →