cprvb - Mathbox for BJ

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

Syntax Definition cprvb 32582

Description: Syntax for the provability predicate.

**Hypothesis**
Ref	Expression
wph

**Assertion**
Ref	Expression
cprvb	Prv

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

Colors of variables: wff setvar class