Metamath Proof Explorer

Theorem nfrd

Description: Consequence of the definition of not-free in a context. (Contributed by Wolf Lammen, 15-Oct-2021)

Ref Expression
Hypothesis nfrd.1 φ x ψ
Assertion nfrd φ x ψ x ψ


Step Hyp Ref Expression
1 nfrd.1 φ x ψ
2 df-nf x ψ x ψ x ψ
3 1 2 sylib φ x ψ x ψ