Metamath Proof Explorer

Theorem nsb

Description: Any substitution in an always false formula is false. (Contributed by Steven Nguyen, 3-May-2023)

Ref Expression
Assertion nsb 
|- ( A. x -. ph -> -. [ t / x ] ph )

Proof

Step Hyp Ref Expression
1 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
2 1 biimpi 
 |-  ( A. x -. ph -> -. E. x ph )
3 spsbe 
 |-  ( [ t / x ] ph -> E. x ph )
4 2 3 nsyl 
 |-  ( A. x -. ph -> -. [ t / x ] ph )