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

Definition df-bi 189
Description: Definition of , in terms of the other logical connectives.
Assertion
Ref Expression
df-bi ((𝜑𝜓) ⧟ ((𝜑𝜓) ∧ (𝜓𝜑)))

Detailed syntax breakdown of Definition df-bi
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 wps . . 3 wff 𝜓
31, 2wbi 188 . 2 wff (𝜑𝜓)
41, 2wim 180 . . 3 wff (𝜑𝜓)
52, 1wim 180 . . 3 wff (𝜓𝜑)
64, 5wand 182 . 2 wff ((𝜑𝜓) ∧ (𝜓𝜑))
73, 6wlb 55 1 wff ((𝜑𝜓) ⧟ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff var nilad
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator