Metamath Proof Explorer

Axiom ax-prv2

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

Ref Expression
Assertion ax-prv2 
|- ( Prv ( ph -> ps ) -> ( Prv ph -> Prv ps ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph 
 |-  ph
1 wps 
 |-  ps
2 0 1 wi 
 |-  ( ph -> ps )
3 2 cprvb 
 |-  Prv ( ph -> ps )
4 0 cprvb 
 |-  Prv ph
5 1 cprvb 
 |-  Prv ps
6 4 5 wi 
 |-  ( Prv ph -> Prv ps )
7 3 6 wi 
 |-  ( Prv ( ph -> ps ) -> ( Prv ph -> Prv ps ) )