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. Based on an idea of Gino Giotto. (Contributed by Wolf Lammen, 29-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 sb6 ⊢ y x φ → ψ ↔ ∀ x x = y → φ → ψ
2 bi2.04 ⊢ φ → x = y → ψ ↔ x = y → φ → ψ
3 2 albii ⊢ ∀ x φ → x = y → ψ ↔ ∀ x x = y → φ → ψ
4 19.21v ⊢ ∀ x φ → x = y → ψ ↔ φ → ∀ x x = y → ψ
5 1 3 4 3bitr2i ⊢ y x φ → ψ ↔ φ → ∀ x x = y → ψ
6 sb6 ⊢ y x ψ ↔ ∀ x x = y → ψ
7 6 imbi2i ⊢ φ → y x ψ ↔ φ → ∀ x x = y → ψ
8 5 7 bitr4i ⊢ y x φ → ψ ↔ φ → y x ψ