ax-prv3 - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-prv3		Structured version Visualization version GIF version

Axiom ax-prv3 34709

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

**Assertion**
Ref	Expression
ax-prv3	⊢ (Prv 𝜑 → Prv Prv 𝜑)

**Detailed syntax breakdown of Axiom ax-prv3**
Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	cprvb 34706	. 2 wff Prv 𝜑
3	2	cprvb 34706	. 2 wff Prv Prv 𝜑
4	2, 3	wi 4	1 wff (Prv 𝜑 → Prv Prv 𝜑)

Colors of variables: wff setvar class

This axiom is referenced by: bj-babygodel 34712 bj-babylob 34713