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

Definition df-pe 149
Description: "Of course" is the dual of "Why not".
Assertion
Ref Expression
df-pe (! 𝜑 ⧟ ~ ? ~ 𝜑)

Detailed syntax breakdown of Definition df-pe
StepHypRef Expression
1 wph . . 3 wff 𝜑
21wpe 148 . 2 wff ! 𝜑
31wneg 3 . . . 4 wff ~ 𝜑
43wne 48 . . 3 wff ? ~ 𝜑
54wneg 3 . 2 wff ~ ? ~ 𝜑
62, 5wlb 55 1 wff (! 𝜑 ⧟ ~ ? ~ 𝜑)
Colors of variables: wff var nilad
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator