Metamath Proof Explorer

Theorem wl-sbrimt

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-sbrimt ⊢ Ⅎ 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 imbi1d ⊢ Ⅎ x φ → y x φ → y x ψ ↔ φ → y x ψ
4 1 3 bitrid ⊢ Ⅎ x φ → y x φ → ψ ↔ φ → y x ψ