This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbrim

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 4-Oct-2016) Avoid ax-10 . (Revised by GG, 20-Nov-2024)

Ref Expression
Hypothesis sbrim.1 ⊢ Ⅎ x φ
Assertion sbrim ⊢ y x φ → ψ ↔ φ → y x ψ

Proof

Step Hyp Ref Expression
1 sbrim.1 ⊢ Ⅎ x φ
2 bi2.04 ⊢ x = t → φ → ψ ↔ φ → x = t → ψ
3 2 albii ⊢ ∀ x x = t → φ → ψ ↔ ∀ x φ → x = t → ψ
4 1 19.21 ⊢ ∀ x φ → x = t → ψ ↔ φ → ∀ x x = t → ψ
5 3 4 bitri ⊢ ∀ x x = t → φ → ψ ↔ φ → ∀ x x = t → ψ
6 5 imbi2i ⊢ t = y → ∀ x x = t → φ → ψ ↔ t = y → φ → ∀ x x = t → ψ
7 bi2.04 ⊢ t = y → φ → ∀ x x = t → ψ ↔ φ → t = y → ∀ x x = t → ψ
8 6 7 bitri ⊢ t = y → ∀ x x = t → φ → ψ ↔ φ → t = y → ∀ x x = t → ψ
9 8 albii ⊢ ∀ t t = y → ∀ x x = t → φ → ψ ↔ ∀ t φ → t = y → ∀ x x = t → ψ
10 dfsb ⊢ y x φ → ψ ↔ ∀ t t = y → ∀ x x = t → φ → ψ
11 dfsb ⊢ y x ψ ↔ ∀ t t = y → ∀ x x = t → ψ
12 11 imbi2i ⊢ φ → y x ψ ↔ φ → ∀ t t = y → ∀ x x = t → ψ
13 19.21v ⊢ ∀ t φ → t = y → ∀ x x = t → ψ ↔ φ → ∀ t t = y → ∀ x x = t → ψ
14 12 13 bitr4i ⊢ φ → y x ψ ↔ ∀ t φ → t = y → ∀ x x = t → ψ
15 9 10 14 3bitr4i ⊢ y x φ → ψ ↔ φ → y x ψ