Theorem sbimd

Description: Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022) Revise df-sb . (Revised by Steven Nguyen, 9-Jul-2023)

	Ref	Expression
Hypotheses	sbimd.1	|- F/ x ph
	sbimd.2	|- ( ph -> ( ps -> ch ) )
Assertion	sbimd	|- ( ph -> ( [ y / x ] ps -> [ y / x ] ch ) )

Proof

Step	Hyp	Ref	Expression
1		sbimd.1	|- F/ x ph
2		sbimd.2	|- ( ph -> ( ps -> ch ) )
3	1 2	alrimi	|- ( ph -> A. x ( ps -> ch ) )
4		spsbim	|- ( A. x ( ps -> ch ) -> ( [ y / x ] ps -> [ y / x ] ch ) )
5	3 4	syl	|- ( ph -> ( [ y / x ] ps -> [ y / x ] ch ) )