ax-epe - Linear Logic Proof Explorer

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

Axiom ax-epe 50

Description: Remove a ? (secretly a !). Inverse of ax-ipe 49.

**Hypothesis**
Ref	Expression
ax-epe.1	⊦ (~ ? 𝜑 ⅋ ? 𝜓)

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

**Detailed syntax breakdown of Axiom ax-epe**
Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wneg 3	. 2 wff ~ 𝜑
3		wps	. . 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: nems 86