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 A A
3 1 2 syl φ A