ax-weak - Linear Logic Proof Explorer

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

Axiom ax-weak 51

Description: ? 𝜑 can be added into any statement.

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

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

Colors of variables: wff var nilad

This axiom is referenced by: (None)