Metamath Proof Explorer

Theorem nsb

Description: Generalization rule for negated wff. (Contributed by Steven Nguyen, 3-May-2023)

Ref Expression
Hypothesis nsb.1 
|- -. ph
Assertion nsb 
|- -. [ x / y ] ph

Proof

Step Hyp Ref Expression
1 nsb.1 
 |-  -. ph
2 1 nex 
 |-  -. E. y ph
3 spsbe 
 |-  ( [ x / y ] ph -> E. y ph )
4 2 3 mto 
 |-  -. [ x / y ] ph