Theorem prvlem2

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

	Ref	Expression
Hypothesis	prvlem2.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	prvlem2	$$⊢Prv\phi \to \left(Prv\psi \to Prv\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		prvlem2.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2	1	prvlem1	$$⊢Prv\phi \to Prv\left(\psi \to \chi \right)$$
3		ax-prv2	$$⊢Prv\left(\psi \to \chi \right)\to \left(Prv\psi \to Prv\chi \right)$$
4	2 3	syl	$$⊢Prv\phi \to \left(Prv\psi \to Prv\chi \right)$$