Axiom ax-prv2

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

	Ref	Expression
Assertion	ax-prv2	⊢ ( Prv ( 𝜑 → 𝜓 ) → ( Prv 𝜑 → Prv 𝜓 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2	0 1	wi	⊢ ( 𝜑 → 𝜓 )
3	2	cprvb	⊢ Prv ( 𝜑 → 𝜓 )
4	0	cprvb	⊢ Prv 𝜑
5	1	cprvb	⊢ Prv 𝜓
6	4 5	wi	⊢ ( Prv 𝜑 → Prv 𝜓 )
7	3 6	wi	⊢ ( Prv ( 𝜑 → 𝜓 ) → ( Prv 𝜑 → Prv 𝜓 ) )