Axiom ax-prv2 32584

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

Assertion

Ref	Expression
ax-prv2	|- (Prv ( ph -> ps ) -> (Prv ph -> Prv ps ) )

Detailed syntax breakdown of Axiom ax-prv2

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff ph
2		wps	. . . 4 wff ps
3	1, 2	wi 4	. . 3 wff ( ph -> ps )
4	3	cprvb 32582	. 2 wff Prv ( ph -> ps )
5	1	cprvb 32582	. . 3 wff Prv ph
6	2	cprvb 32582	. . 3 wff Prv ps
7	5, 6	wi 4	. 2 wff (Prv ph -> Prv ps )
8	4, 7	wi 4	1 wff (Prv ( ph -> ps ) -> (Prv ph -> Prv ps ) )

This axiom is referenced by:  prvlem1  32586  prvlem2  32587