ax-ipe - Linear Logic Proof Explorer

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

Axiom ax-ipe 49

Description: Add a ? (secretly a !). Inverse of ax-epe 50.

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

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

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

Colors of variables: wff var nilad

This axiom is referenced by: nems 86