ax-1re - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ax-1re		Unicode version

Axiom ax-1re 7990

Description: 1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 7946. Proofs should use 1re 8042 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)

**Assertion**
Ref	Expression
ax-1re

**Detailed syntax breakdown of Axiom ax-1re**
Step	Hyp	Ref	Expression
1		c1 7897	. 2
2		cr 7895	. 2
3	1, 2	wcel 2167	1

Colors of variables: wff set class

This axiom is referenced by: 1re 8042

W3C validator