Theorem prvlem2

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

	Ref	Expression
Hypothesis	prvlem2.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion	prvlem2	⊢ ( Prv 𝜑 → ( Prv 𝜓 → Prv 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		prvlem2.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2	1	prvlem1	⊢ ( Prv 𝜑 → Prv ( 𝜓 → 𝜒 ) )
3		ax-prv2	⊢ ( Prv ( 𝜓 → 𝜒 ) → ( Prv 𝜓 → Prv 𝜒 ) )
4	2 3	syl	⊢ ( Prv 𝜑 → ( Prv 𝜓 → Prv 𝜒 ) )