This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem spsbim

Description: Distribute substitution over implication. Closed form of sbimi . Specialization of implication. (Contributed by NM, 5-Aug-1993) (Proof shortened by Andrew Salmon, 25-May-2011) Revise df-sb . (Revised by BJ, 22-Dec-2020) (Proof shortened by Steven Nguyen, 24-Jul-2023)

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

Proof

Step Hyp Ref Expression
1 stdpc4 
 |-  ( A. x ( ph -> ps ) -> [ t / x ] ( ph -> ps ) )
2 sbi1 
 |-  ( [ t / x ] ( ph -> ps ) -> ( [ t / x ] ph -> [ t / x ] ps ) )
3 1 2 syl 
 |-  ( A. x ( ph -> ps ) -> ( [ t / x ] ph -> [ t / x ] ps ) )