Axiom ax-prv3

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

	Ref	Expression
Assertion	ax-prv3	$$⊢Prv\phi \to PrvPrv\phi$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1	0	cprvb	$$wffPrv\phi$$
2	1	cprvb	$$wffPrvPrv\phi$$
3	1 2	wi	$$wff\left(Prv\phi \to PrvPrv\phi \right)$$