Theorem sbi1

Description: Distribute substitution over implication. (Contributed by NM, 14-May-1993) Remove dependencies on axioms. (Revised by Steven Nguyen, 24-Jul-2023) Definition df-sb changed. (Revised by Wolf Lammen, 5-Jun-2026)

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

Proof

Step	Hyp	Ref	Expression
1		sbi1lem	|- ( ( [ y / x ] ( ph -> ps ) /\ [ y / x ] ph ) -> A. u ( u = y -> A. x ( x = u -> ps ) ) )
2		sbi1lem	|- ( ( [ y / x ] ( ph -> ps ) /\ [ y / x ] ph ) -> A. z ( z = y -> A. x ( x = z -> ps ) ) )
3		df-sb	|- ( [ y / x ] ps <-> ( A. u ( u = y -> A. x ( x = u -> ps ) ) /\ A. z ( z = y -> A. x ( x = z -> ps ) ) ) )
4	1 2 3	sylanbrc	|- ( ( [ y / x ] ( ph -> ps ) /\ [ y / x ] ph ) -> [ y / x ] ps )
5	4	ex	|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )