Axiom ax-prv2 36600

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

Assertion

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

Detailed syntax breakdown of Axiom ax-prv2

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		wps	. . . 4 wff 𝜓
3	1, 2	wi 4	. . 3 wff (𝜑 → 𝜓)
4	3	cprvb 36598	. 2 wff Prv (𝜑 → 𝜓)
5	1	cprvb 36598	. . 3 wff Prv 𝜑
6	2	cprvb 36598	. . 3 wff Prv 𝜓
7	5, 6	wi 4	. 2 wff (Prv 𝜑 → Prv 𝜓)
8	4, 7	wi 4	1 wff (Prv (𝜑 → 𝜓) → (Prv 𝜑 → Prv 𝜓))

This axiom is referenced by:  prvlem1  36602  prvlem2  36603