Theorem sbim

Description: Implication inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993)

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

Proof

Step	Hyp	Ref	Expression
1		sbi1	|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
2		sbi2	|- ( ( [ y / x ] ph -> [ y / x ] ps ) -> [ y / x ] ( ph -> ps ) )
3	1 2	impbii	|- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )