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

Axiom ax-almd 324
Description: Quantified multiplicative disjunction. This "distributes" a quantifier over linear implication.
Assertion
Ref Expression
ax-almd (∀x(𝜑𝜓) ⊸ (∀x𝜑 ⊸ ∀x𝜓))

Detailed syntax breakdown of Axiom ax-almd
StepHypRef Expression
1 wph . . . 4 wff 𝜑
2 wps . . . 4 wff 𝜓
31, 2wli 61 . . 3 wff (𝜑𝜓)
4 vx . . 3 var x
53, 4wal 318 . 2 wffx(𝜑𝜓)
61, 4wal 318 . . 3 wffx𝜑
72, 4wal 318 . . 3 wffx𝜓
86, 7wli 61 . 2 wff (∀x𝜑 ⊸ ∀x𝜓)
95, 8wli 61 1 wff (∀x(𝜑𝜓) ⊸ (∀x𝜑 ⊸ ∀x𝜓))
Colors of variables: wff var nilad
This axiom is referenced by: (None)
  Copyright terms: Public domain W3C validator