Metamath Proof Explorer

Axiom ax-prv3

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

Ref Expression
Assertion ax-prv3 
|- ( Prv ph -> Prv Prv ph )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph 
 |-  ph
1 0 cprvb 
 |-  Prv ph
2 1 cprvb 
 |-  Prv Prv ph
3 1 2 wi 
 |-  ( Prv ph -> Prv Prv ph )