ax-prv1 - Mathbox for BJ

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

Axiom ax-prv1 37302

Description: First property of three of the provability predicate. (Contributed by BJ, 3-Apr-2019.)

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

**Assertion**
Ref	Expression
ax-prv1	⊢ Prv 𝜑

**Detailed syntax breakdown of Axiom ax-prv1**
Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2	1	cprvb 37301	1 wff Prv 𝜑

Colors of variables: wff setvar class

This axiom is used by: prvlem1 37305 bj-babygodel 37307 bj-babylob 37308