ax-top - Linear Logic Proof Explorer

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

Axiom ax-top 31

Description: Anything can turn into ⊤.

**Assertion**
Ref	Expression
ax-top	⊦ (~ 𝜑 ⅋ ⊤)

**Detailed syntax breakdown of Axiom ax-top**
Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wneg 3	. 2 wff ~ 𝜑
3		wtop 29	. 2 wff ⊤
4	2, 3	wmd 2	1 wff (~ 𝜑 ⅋ ⊤)

Colors of variables: wff var nilad

This axiom is referenced by: itopi 41