Theorem sbi2

Description: Introduction of implication into substitution. (Contributed by NM, 14-May-1993)

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

Proof

Step	Hyp	Ref	Expression
1		sbn	|- ( [ y / x ] -. ph <-> -. [ y / x ] ph )
2		pm2.21	|- ( -. ph -> ( ph -> ps ) )
3	2	sbimi	|- ( [ y / x ] -. ph -> [ y / x ] ( ph -> ps ) )
4	1 3	sylbir	|- ( -. [ y / x ] ph -> [ y / x ] ( ph -> ps ) )
5		ax-1	|- ( ps -> ( ph -> ps ) )
6	5	sbimi	|- ( [ y / x ] ps -> [ y / x ] ( ph -> ps ) )
7	4 6	ja	|- ( ( [ y / x ] ph -> [ y / x ] ps ) -> [ y / x ] ( ph -> ps ) )