Metamath Proof Explorer

Axiom ax-prv1

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

Ref Expression
Hypothesis ax-prv1.1 
|- ph
Assertion ax-prv1 
|- Prv ph

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph 
 |-  ph
1 0 cprvb 
 |-  Prv ph