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

Definition df-im 181
Description: Definition of . It's but with some ! splashed in for good measure. Note that only 𝜑 needs the exponential. When this statement is beneath a ! or at the top level, this is equivalent to both sides having the exponential, because of
Assertion
Ref Expression
df-im ((𝜑𝜓) ⧟ (! 𝜑𝜓))

Detailed syntax breakdown of Definition df-im
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wim 180 . 2 wff (𝜑𝜓)
41wpe 148 . . 3 wff ! 𝜑
54, 2wli 61 . 2 wff (! 𝜑𝜓)
63, 5wlb 55 1 wff ((𝜑𝜓) ⧟ (! 𝜑𝜓))
Colors of variables: wff var nilad
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator