Metamath Proof Explorer


Theorem sblim

Description: Substitution in an implication with a variable not free in the consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013) (Revised by Mario Carneiro, 4-Oct-2016)

Ref Expression
Hypothesis sblim.1
|- F/ x ps
Assertion sblim
|- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> ps ) )

Proof

Step Hyp Ref Expression
1 sblim.1
 |-  F/ x ps
2 sbim
 |-  ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
3 1 sbf
 |-  ( [ y / x ] ps <-> ps )
4 3 imbi2i
 |-  ( ( [ y / x ] ph -> [ y / x ] ps ) <-> ( [ y / x ] ph -> ps ) )
5 2 4 bitri
 |-  ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> ps ) )