Theorem sbiedvw 2128

Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2126). Version of sbied 2533 and sbiedv 2534 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 2123	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
2		sbiedvw.1	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))
3	2	expcom 418	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 → (𝜓 ↔ 𝜒)))
4	3	pm5.74d 276	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
5	4	sbievw 2126	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
6	1, 5	bitr3i 280	. 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → 𝜒))
7	6	pm5.74ri 275	1 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  [wsb 2094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2095

This theorem is referenced by:  2sbievw  2129  iscatd2  17736  bj-elabd2ALT  37527