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

Definition df-nnu 245
Description: Definition of the dual creation operator.
Assertion
Ref Expression
df-nnu (∇x𝜑 ⧟ ~ νx~ 𝜑)

Detailed syntax breakdown of Definition df-nnu
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 var x
31, 2wnnu 242 . 2 wffx𝜑
41wneg 3 . . . 4 wff ~ 𝜑
54, 2wnu 206 . . 3 wff νx~ 𝜑
65wneg 3 . 2 wff ~ νx~ 𝜑
73, 6wlb 55 1 wff (∇x𝜑 ⧟ ~ νx~ 𝜑)
Colors of variables: wff var nilad
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator