Metamath Proof Explorer

Theorem wl-sblimt

Description: Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim . (Contributed by Wolf Lammen, 26-Jul-2019)

Ref Expression
Assertion wl-sblimt ⊢ Ⅎ x ψ → y x φ → ψ ↔ y x φ → ψ

Proof

Step Hyp Ref Expression
1 sbim ⊢ y x φ → ψ ↔ y x φ → y x ψ
2 sbft ⊢ Ⅎ x ψ → y x ψ ↔ ψ
3 2 imbi2d ⊢ Ⅎ x ψ → y x φ → y x ψ ↔ y x φ → ψ
4 1 3 bitrid ⊢ Ⅎ x ψ → y x φ → ψ ↔ y x φ → ψ