Let A, B and C be given.

Assume H.

Apply (H (A ∧ (B ∧ C))) to the current goal.

Assume Hab Hc.

Apply (Hab (A ∧ (B ∧ C))) to the current goal.

Assume Ha Hb.

Apply andI to the current goal.

An exact proof term for the current goal is Ha.

Apply andI to the current goal.

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is Hc.

∎