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

Metamath Proof Explorer

Theorem sbi1

Description: Distribute substitution over implication. (Contributed by NM, 14-May-1993) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023)

Ref Expression
Assertion sbi1 
|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )

Proof

Step Hyp Ref Expression
1 dfsb 
 |-  ( [ y / x ] ( ph -> ps ) <-> A. z ( z = y -> A. x ( x = z -> ( ph -> ps ) ) ) )
2 ax-2 
 |-  ( ( x = z -> ( ph -> ps ) ) -> ( ( x = z -> ph ) -> ( x = z -> ps ) ) )
3 2 al2imi 
 |-  ( A. x ( x = z -> ( ph -> ps ) ) -> ( A. x ( x = z -> ph ) -> A. x ( x = z -> ps ) ) )
4 3 imim3i 
 |-  ( ( z = y -> A. x ( x = z -> ( ph -> ps ) ) ) -> ( ( z = y -> A. x ( x = z -> ph ) ) -> ( z = y -> A. x ( x = z -> ps ) ) ) )
5 4 al2imi 
 |-  ( A. z ( z = y -> A. x ( x = z -> ( ph -> ps ) ) ) -> ( A. z ( z = y -> A. x ( x = z -> ph ) ) -> A. z ( z = y -> A. x ( x = z -> ps ) ) ) )
6 dfsb 
 |-  ( [ y / x ] ph <-> A. z ( z = y -> A. x ( x = z -> ph ) ) )
7 dfsb 
 |-  ( [ y / x ] ps <-> A. z ( z = y -> A. x ( x = z -> ps ) ) )
8 5 6 7 3imtr4g 
 |-  ( A. z ( z = y -> A. x ( x = z -> ( ph -> ps ) ) ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
9 1 8 sylbi 
 |-  ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )