Theorem sbimvOLD

Description: Obsolete version of sbim as of 24-Jul-2023. Substitution distributes over implication. Version of sbim with a disjoint variable condition, not requiring ax-13 . (Contributed by Wolf Lammen, 18-Jan-2023) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sbi1vOLD	|- ( [ 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 ) )