Theorem prvlem2

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

	Ref	Expression
Hypothesis	prvlem2.1	|- ( ph -> ( ps -> ch ) )
Assertion	prvlem2	|- ( Prv ph -> ( Prv ps -> Prv ch ) )

Proof

Step	Hyp	Ref	Expression
1		prvlem2.1	|- ( ph -> ( ps -> ch ) )
2	1	prvlem1	|- ( Prv ph -> Prv ( ps -> ch ) )
3		ax-prv2	|- ( Prv ( ps -> ch ) -> ( Prv ps -> Prv ch ) )
4	2 3	syl	|- ( Prv ph -> ( Prv ps -> Prv ch ) )