wff-neg - bfol.mm Proof Explorer

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

Syntax Definition wff-neg 9

Description: If '𝜑' is well formed formula, then '¬ 𝜑' is a well formed formula.

**Hypothesis**
Ref	Expression
wff-ph	wff 𝜑

**Assertion**
Ref	Expression
wff-neg	wff ¬ 𝜑

This syntax is primitive. The first axiom using it is ax-L3 13.

Colors of variables: wff objvar term class