Axiom ax-prv3

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

	Ref	Expression
Assertion	ax-prv3	⊢ ( Prv 𝜑 → Prv Prv 𝜑 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1	0	cprvb	⊢ Prv 𝜑
2	1	cprvb	⊢ Prv Prv 𝜑
3	1 2	wi	⊢ ( Prv 𝜑 → Prv Prv 𝜑 )