This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0red

Description: The number 0 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018)

Ref Expression
Assertion 0red ( 𝜑 → 0 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 1 a1i ⊢ ( 𝜑 → 0 ∈ ℝ )