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 x ψ
Assertion sblim y x φ ψ y x φ ψ


Step Hyp Ref Expression
1 sblim.1 x ψ
2 sbim y x φ ψ y x φ y x ψ
3 1 sbf y x ψ ψ
4 3 imbi2i y x φ y x ψ y x φ ψ
5 2 4 bitri y x φ ψ y x φ ψ