Metamath Proof Explorer


Theorem nfnd

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

Ref Expression
Hypothesis nfnd.1 φ x ψ
Assertion nfnd φ x ¬ ψ

Proof

Step Hyp Ref Expression
1 nfnd.1 φ x ψ
2 nfnt x ψ x ¬ ψ
3 1 2 syl φ x ¬ ψ