cprvb - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cprvb		Structured version Visualization version GIF version

Syntax Definition cprvb 33926

Description: Syntax for the provability predicate.

**Hypothesis**
Ref	Expression
wph	wff 𝜑

**Assertion**
Ref	Expression
cprvb	wff Prv 𝜑

This syntax is primitive. The first axiom using it is ax-prv1 33927.

Colors of variables: wff setvar class