Metamath Proof Explorer

Theorem sbrimvw

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim based on fewer axioms, but with more disjoint variable conditions. (Contributed by Wolf Lammen, 29-Jan-2024) Remove DV condition. (Revised by Wolf Lammen, 5-Jun-2026)

Ref Expression
Assertion sbrimvw ⊢ y x φ → ψ ↔ φ → y x ψ

Proof

Step Hyp Ref Expression
1 sbv ⊢ y x φ ↔ φ
2 sbi1 ⊢ y x φ → ψ → y x φ → y x ψ
3 1 2 biimtrrid ⊢ y x φ → ψ → φ → y x ψ
4 sbv ⊢ y x ¬ φ ↔ ¬ φ
5 pm2.21 ⊢ ¬ φ → φ → ψ
6 5 sbimi ⊢ y x ¬ φ → y x φ → ψ
7 4 6 sylbir ⊢ ¬ φ → y x φ → ψ
8 ax-1 ⊢ ψ → φ → ψ
9 8 sbimi ⊢ y x ψ → y x φ → ψ
10 7 9 ja ⊢ φ → y x ψ → y x φ → ψ
11 3 10 impbii ⊢ y x φ → ψ ↔ φ → y x ψ