Axiom ax-prv1

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

	Ref	Expression
Hypothesis	ax-prv1.1	⊢ 𝜑
Assertion	ax-prv1	⊢ Prv 𝜑

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1	0	cprvb	⊢ Prv 𝜑