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 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion nfnegd ( 𝜑 → Ⅎ 𝑥 - 𝐴 )

Proof

Step Hyp Ref Expression
1 nfnegd.1 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2 df-neg ⊢ - 𝐴 = ( 0 − 𝐴 )
3 nfcvd ⊢ ( 𝜑 → Ⅎ 𝑥 0 )
4 nfcvd ⊢ ( 𝜑 → Ⅎ 𝑥 − )
5 3 4 1 nfovd ⊢ ( 𝜑 → Ⅎ 𝑥 ( 0 − 𝐴 ) )
6 2 5 nfcxfrd ⊢ ( 𝜑 → Ⅎ 𝑥 - 𝐴 )