acasb - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > acasb		Structured version

Theorem acasb 138

Description: & is associative.

**Assertion**
Ref	Expression
acasb	⊦ (((𝜑 & 𝜓) & 𝜒) ⧟ (𝜓 & (𝜓 & 𝜒)))

**Proof of Theorem acasb**
Step	Hyp	Ref	Expression

Colors of variables: wff var nilad

Syntax hints: & wac 30 ⧟ wlb 55

WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)