∧-Intro: Proving a conjunction

The rule

To prove P ∧ Q, prove P and prove Q separately.

Conjunction introduction requires two premises — one for each conjunct. You must supply independent proofs of both P and Q. The two sub-proofs sit side by side above the horizontal bar.

Gentzen notation

  P       Q
————————— ∧-Intro
   P ∧ Q

Watch the proof build

In any prover

Prover	Syntax
Lean 4	`constructor` or `exact ⟨hp, hq⟩`
Coq	`split`
Agda	`hp , hq`

Your turn

Prove P ∧ (Q ∧ R) from assumptions P, Q, R. How many ∧-Intro rules do you need?

Hint

You need to build Q ∧ R first (one ∧-Intro), then combine P with Q ∧ R (another ∧-Intro).

Solution

          Q       R
         ————————— ∧-Intro
  P       Q ∧ R
————————————— ∧-Intro
  P ∧ (Q ∧ R)

You need two ∧-Intro rules: one to build Q ∧ R, and one to build P ∧ (Q ∧ R).

← Hypothetical syllogism ∧-Elim →