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		df-sb	|- ( [ 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		df-sb	|- ( [ y / x ] ph <-> A. z ( z = y -> A. x ( x = z -> ph ) ) )
7		df-sb	|- ( [ 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 ) )