wal - Linear Logic Proof Explorer

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

Syntax Definition wal 318

Description: Universal quantifier. Characterized by ax-genOLD 323, ax-almd 324, ax-dis 325, ax-ex 326, ax-negf 330, ax-alcom 331.

**Hypotheses**
Ref	Expression
wph	wff 𝜑
vx	var x

**Assertion**
Ref	Expression
wal	wff ∀x𝜑

This syntax is primitive. The first axiom using it is ax-genOLD 323.

Colors of variables: wff var nilad