Theorem sbiedvw 2094

Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2092). Version of sbied 2507 and sbiedv 2508 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by GG, 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 2090	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
2		sbiedvw.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))
3	2	expcom 413	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm5.74d 273	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
5	4	sbievw 2092	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
6	1, 5	bitr3i 277	. 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → 𝜒))
7	6	pm5.74ri 272	1 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  [wsb 2063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064

This theorem is referenced by:  2sbievw  2095  iscatd2  17725  bj-elabd2ALT  36927