∧-Elim: Taking a conjunction apart

The rules

From P ∧ Q, you can extract P (project left) or Q (project right).

There are two elimination rules for conjunction — one for each component. They are the inverse of ∧-Intro: where introduction builds a pair, elimination takes it apart.

Gentzen notation

 P ∧ Q              P ∧ Q
—————— ∧-Elim&sub1;     —————— ∧-Elim&sub2;
   P                  Q

Watch the proof build

In any prover

Prover	Syntax
Lean 4	`exact h.1` / `exact h.2`
Coq	`destruct H as [HP HQ]`
Agda	`proj&sub1; h` / `proj&sub2; h`

Your turn

Prove (P ∧ Q) ∧ R → P ∧ (Q ∧ R). You will need both ∧-Intro and ∧-Elim.

Hint

Start with →-Intro to assume (P ∧ Q) ∧ R. Then use ∧-Elim to extract P ∧ Q and R. From P ∧ Q, extract P and Q individually. Finally, rebuild as P ∧ (Q ∧ R) using two ∧-Intro applications.

Solution

               [(P ∧ Q) ∧ R]¹
               ———————————— ∧-Elim&sub1;
 [(P∧Q)∧R]¹      P ∧ Q           [(P∧Q)∧R]¹
 ———————— ∧-Elim&sub1;  ————— ∧-Elim&sub2;  ———————— ∧-Elim&sub2;
   P ∧ Q          Q               R
  ————— ∧-Elim&sub1;  ————————————— ∧-Intro
     P              Q ∧ R
    ————————————————— ∧-Intro
         P ∧ (Q ∧ R)
———————————————————————— →-Intro¹
   (P ∧ Q) ∧ R → P ∧ (Q ∧ R)

See also: Logic §03 — Conjunction

← ∧-Intro ∨-Intro →