Metamath Proof Explorer


Theorem prvlem1

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

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

Proof

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