Metamath Proof Explorer

Theorem sbrimvwOLD

Description: Obsolete version of sbrimvw as of 5-Jun-2026. (Contributed by Wolf Lammen, 29-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbrimvwOLD ⊢ 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 ψ