ax-genOLD - Linear Logic Proof Explorer

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

Axiom ax-genOLD 323

Description: Axiom of generalization. Universal quantifiers can be freely added to the start of an expression.

**Hypothesis**
Ref	Expression
ax-genOLD.1	⊦ 𝜑

**Assertion**
Ref	Expression
ax-genOLD	⊦ ∀x𝜑

**Detailed syntax breakdown of Axiom ax-genOLD**
Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		vx	. 2 var x
3	1, 2	wal 318	1 wff ∀x𝜑

Colors of variables: wff var nilad

This axiom is referenced by: (None)