Theorem sb2imi

Description: Distribute substitution over implication. Compare al2imi . (Contributed by Steven Nguyen, 13-Aug-2023)

	Ref	Expression
Hypothesis	sb2imi.1	|- ( ph -> ( ps -> ch ) )
Assertion	sb2imi	|- ( [ t / x ] ph -> ( [ t / x ] ps -> [ t / x ] ch ) )

Proof

Step	Hyp	Ref	Expression
1		sb2imi.1	|- ( ph -> ( ps -> ch ) )
2	1	sbimi	|- ( [ t / x ] ph -> [ t / x ] ( ps -> ch ) )
3		sbi1	|- ( [ t / x ] ( ps -> ch ) -> ( [ t / x ] ps -> [ t / x ] ch ) )
4	2 3	syl	|- ( [ t / x ] ph -> ( [ t / x ] ps -> [ t / x ] ch ) )