Metamath Proof Explorer

Theorem nf5ri

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 15-Mar-2023)

Ref Expression
Hypothesis nf5ri.1 x φ
Assertion nf5ri φ x φ


Step Hyp Ref Expression
1 nf5ri.1 x φ
2 1 nfri x φ x φ
3 2 19.23bi φ x φ