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

Metamath Proof Explorer

Theorem nfnegd

Description: Deduction version of nfneg . (Contributed by NM, 29-Feb-2008) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypothesis nfnegd.1 ⊢ φ → Ⅎ _ x A
Assertion nfnegd ⊢ φ → Ⅎ _ x − A

Proof

Step Hyp Ref Expression
1 nfnegd.1 ⊢ φ → Ⅎ _ x A
2 df-neg ⊢ − A = 0 − A
3 nfcvd ⊢ φ → Ⅎ _ x 0
4 nfcvd ⊢ φ → Ⅎ _ x −
5 3 4 1 nfovd ⊢ φ → Ⅎ _ x 0 − A
6 2 5 nfcxfrd ⊢ φ → Ⅎ _ x − A