Theorem sbiedvw 2132

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094

This theorem is referenced by:  2sbievw  2133  iscatd2  17727  bj-elabd2ALT  37422