Theorem sbi1vOLD

Description: Obsolete version of sbi1 as of 24-Jul-2023. Move implication out of substitution. Version of sbi1 with a disjoint variable condition, not requiring ax-13 . (Contributed by Wolf Lammen, 18-Jan-2023) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sb4vOLD	|- ( [ y / x ] ( ph -> ps ) -> A. x ( x = y -> ( ph -> ps ) ) )
2		sb4vOLD	|- ( [ y / x ] ph -> A. x ( x = y -> ph ) )
3		ax-2	|- ( ( x = y -> ( ph -> ps ) ) -> ( ( x = y -> ph ) -> ( x = y -> ps ) ) )
4	3	al2imi	|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ( x = y -> ph ) -> A. x ( x = y -> ps ) ) )
5		sb2vOLD	|- ( A. x ( x = y -> ps ) -> [ y / x ] ps )
6	2 4 5	syl56	|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
7	1 6	syl	|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )