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

Metamath Proof Explorer

Theorem absidd

Description: A nonnegative number is its own absolute value. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses resqrcld.1 ⊢ φ → A ∈ ℝ
resqrcld.2 ⊢ φ → 0 ≤ A
Assertion absidd ⊢ φ → A = A

Proof

Step Hyp Ref Expression
1 resqrcld.1 ⊢ φ → A ∈ ℝ
2 resqrcld.2 ⊢ φ → 0 ≤ A
3 absid ⊢ A ∈ ℝ ∧ 0 ≤ A → A = A
4 1 2 3 syl2anc ⊢ φ → A = A