ax-GEN - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > ax-GEN

Axiom ax-GEN 15

Description: Rule of Generalization.

**Hypothesis**
Ref	Expression
ax-GEN.1	⊢ 𝜑

**Assertion**
Ref	Expression
ax-GEN	⊢ ∀𝑥𝜑

**Detailed syntax breakdown of Axiom ax-GEN**
Step	Hyp	Ref	Expression
1		wff-ph	. 2 wff 𝜑
2		objvar-x	. 2 objvar 𝑥
3	1, 2	wff-forall 8	1 wff ∀𝑥𝜑

Colors of variables: wff objvar term class