ax-pemc - Linear Logic Proof Explorer

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

Axiom ax-pemc 53

Description: ! 1. This is needed to let ax-ipe 49 and ax-epe 50 work on single items.

**Assertion**
Ref	Expression
ax-pemc	⊦ ~ ? ⊥

**Detailed syntax breakdown of Axiom ax-pemc**
Step	Hyp	Ref	Expression
1		wbot 1	. . 3 wff ⊥
2	1	wne 48	. 2 wff ? ⊥
3	2	wneg 3	1 wff ~ ? ⊥

Colors of variables: wff var nilad

This axiom is referenced by: (None)