Metamath Proof Explorer

Theorem sbiedvw

Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw ). Version of sbied and sbiedv with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994) (Revised by GG, 29-Jan-2024)

Ref Expression
Hypothesis sbiedvw.1 ⊢ φ ∧ x = y → ψ ↔ χ
Assertion sbiedvw ⊢ φ → y x ψ ↔ χ

Proof

Step Hyp Ref Expression
1 sbiedvw.1 ⊢ φ ∧ x = y → ψ ↔ χ
2 sbrimvw ⊢ y x φ → ψ ↔ φ → y x ψ
3 1 expcom ⊢ x = y → φ → ψ ↔ χ
4 3 pm5.74d ⊢ x = y → φ → ψ ↔ φ → χ
5 4 sbievw ⊢ y x φ → ψ ↔ φ → χ
6 2 5 bitr3i ⊢ φ → y x ψ ↔ φ → χ
7 6 pm5.74ri ⊢ φ → y x ψ ↔ χ