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 φ → ψ

Proof

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 φ → ψ