Axiom ax-prv2

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

	Ref	Expression
Assertion	ax-prv2	$$⊢Prv\left(\phi \to \psi \right)\to \left(Prv\phi \to Prv\psi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	0 1	wi	$$wff\left(\phi \to \psi \right)$$
3	2	cprvb	$$wffPrv\left(\phi \to \psi \right)$$
4	0	cprvb	$$wffPrv\phi$$
5	1	cprvb	$$wffPrv\psi$$
6	4 5	wi	$$wff\left(Prv\phi \to Prv\psi \right)$$
7	3 6	wi	$$wff\left(Prv\left(\phi \to \psi \right)\to \left(Prv\phi \to Prv\psi \right)\right)$$