Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Provability logic
ax-prv1
Next ⟩
ax-prv2
Metamath Proof Explorer
Ascii
Unicode
Axiom
ax-prv1
Description:
First property of three of the provability predicate.
(Contributed by
BJ
, 3-Apr-2019)
Ref
Expression
Hypothesis
ax-prv1.1
⊢
φ
Assertion
ax-prv1
⊢
Prv
φ
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
wph
wff
φ
1
0
cprvb
wff
Prv
φ