Metamath Proof Explorer


Theorem prvlem1

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

Ref Expression
Hypothesis prvlem1.1 ( 𝜑𝜓 )
Assertion prvlem1 ( Prv 𝜑 → Prv 𝜓 )

Proof

Step Hyp Ref Expression
1 prvlem1.1 ( 𝜑𝜓 )
2 1 ax-prv1 Prv ( 𝜑𝜓 )
3 ax-prv2 ( Prv ( 𝜑𝜓 ) → ( Prv 𝜑 → Prv 𝜓 ) )
4 2 3 ax-mp ( Prv 𝜑 → Prv 𝜓 )