ax-bj-d0cl - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-bj-d0cl		GIF version

Axiom ax-bj-d0cl 16640

Description: Axiom for Δ₀-classical logic. (Contributed by BJ, 2-Jan-2020.) New usage is discouraged since this statement is not intuitionnistic. (New usage is discouraged.)

**Hypothesis**
Ref	Expression
ax-bj-d0class.bd	⊢ BOUNDED 𝜑

**Assertion**
Ref	Expression
ax-bj-d0cl	⊢ DECID 𝜑

**Detailed syntax breakdown of Axiom ax-bj-d0cl**
Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2	1	wdc 842	1 wff DECID 𝜑

Colors of variables: wff set class

This axiom is referenced by: bj-d0clsepcl 16641

W3C validator