Metamath Proof Explorer


Theorem renegcld

Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis renegcld.1 φA
Assertion renegcld φA

Proof

Step Hyp Ref Expression
1 renegcld.1 φA
2 renegcl AA
3 1 2 syl φA