ax-contr - Linear Logic Proof Explorer

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

Axiom ax-contr 52

Description: ? 𝜑 can be contracted.

**Assertion**
Ref	Expression
ax-contr	⊦ (~ (? 𝜑 ⅋ ? 𝜑) ⅋ ? 𝜑)

**Detailed syntax breakdown of Axiom ax-contr**
Step	Hyp	Ref	Expression
1		wph	. . . . 5 wff 𝜑
2	1	wne 48	. . . 4 wff ? 𝜑
3	2, 2	wmd 2	. . 3 wff (? 𝜑 ⅋ ? 𝜑)
4	3	wneg 3	. 2 wff ~ (? 𝜑 ⅋ ? 𝜑)
5	4, 2	wmd 2	1 wff (~ (? 𝜑 ⅋ ? 𝜑) ⅋ ? 𝜑)

Colors of variables: wff var nilad

This axiom is referenced by: (None)