Metamath Proof Explorer

Theorem nfnd

Description: Deduction associated with nfnt . (Contributed by Mario Carneiro, 24-Sep-2016)

Ref Expression
Hypothesis nfnd.1 
|- ( ph -> F/ x ps )
Assertion nfnd 
|- ( ph -> F/ x -. ps )

Proof

Step Hyp Ref Expression
1 nfnd.1 
 |-  ( ph -> F/ x ps )
2 nfnt 
 |-  ( F/ x ps -> F/ x -. ps )
3 1 2 syl 
 |-  ( ph -> F/ x -. ps )