Theorem sbiedvw 2099

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

Hypothesis

Ref	Expression
sbiedvw.1	⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
sbiedvw	⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)   𝜒(𝑦)

Proof of Theorem sbiedvw

Step	Hyp	Ref	Expression
1		sbrimvw 2097	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
2		sbiedvw.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))
3	2	expcom 413	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm5.74d 272	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
5	4	sbievw 2098	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
6	1, 5	bitr3i 276	. 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → 𝜒))
7	6	pm5.74ri 271	1 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  [wsb 2070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-sb 2071

This theorem is referenced by:  2sbievw  2100  iscatd2  17371  bj-elabd2ALT  35092