Metamath Proof Explorer

Theorem sbn1

Description: One direction of sbn , using fewer axioms. Compare 19.2 . (Contributed by Steven Nguyen, 18-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 nsb 
 |-  ( A. x -. F. -> -. [ t / x ] F. )
2 fal 
 |-  -. F.
3 1 2 mpg 
 |-  -. [ t / x ] F.
4 pm2.21 
 |-  ( -. ph -> ( ph -> F. ) )
5 4 sb2imi 
 |-  ( [ t / x ] -. ph -> ( [ t / x ] ph -> [ t / x ] F. ) )
6 3 5 mtoi 
 |-  ( [ t / x ] -. ph -> -. [ t / x ] ph )