Theorem ifeqeqxdc 3673

Description: An equality theorem tailored for ballotfilemsf1o 13201. (Contributed by Thierry Arnoux, 14-Apr-2017.)

Hypotheses

Ref	Expression
ifeqeqx.1	⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶)
ifeqeqx.2	⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎)
ifeqeqx.3	⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃))
ifeqeqx.4	⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓))
ifeqeqx.5	⊢ (𝜑 → 𝑎 = 𝐶)
ifeqeqx.6	⊢ ((𝜑 ∧ 𝜓) → 𝜃)
ifeqeqx.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
ifeqeqx.x	⊢ (𝜑 → 𝑋 ∈ 𝑊)
ifeqeqxdc.dc	⊢ (𝜑 → DECID 𝜓)

Assertion

Ref	Expression
ifeqeqxdc	⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))

Distinct variable groups:   𝑥,𝑎   𝑥,𝐶   𝑥,𝑋   𝑥,𝑌   𝑥,𝑉   𝑥,𝑊   𝜓,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑎)   𝜓(𝑎)   𝜒(𝑥,𝑎)   𝜃(𝑎)   𝐴(𝑥,𝑎)   𝐵(𝑥,𝑎)   𝐶(𝑎)   𝑉(𝑎)   𝑊(𝑎)   𝑋(𝑎)   𝑌(𝑎)

Proof of Theorem ifeqeqxdc

Step	Hyp	Ref	Expression
1		eqeq2 2244	. 2 ⊢ (𝐴 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐴 ↔ 𝑎 = if(𝜒, 𝐴, 𝐵)))
2		eqeq2 2244	. 2 ⊢ (𝐵 = if(𝜒, 𝐴, 𝐵) → (𝑎 = 𝐵 ↔ 𝑎 = if(𝜒, 𝐴, 𝐵)))
3		simplr 529	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
4		simpll 527	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜑)
5		simpr 110	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝜒)
6		sbceq1a 3055	. . . . . 6 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
7	6	biimpd 144	. . . . 5 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝜒 → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
8	3, 5, 7	sylc 62	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
9		dfsbcq 3047	. . . . . 6 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ([𝑋 / 𝑥]𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
10		csbeq1 3144	. . . . . . 7 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ⦋𝑋 / 𝑥⦌𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)
11	10	eqeq2d 2246	. . . . . 6 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑋 / 𝑥⦌𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))
12	9, 11	imbi12d 234	. . . . 5 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (([𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)))
13		dfsbcq 3047	. . . . . 6 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ([𝑌 / 𝑥]𝜒 ↔ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
14		csbeq1 3144	. . . . . . 7 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ⦋𝑌 / 𝑥⦌𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)
15	14	eqeq2d 2246	. . . . . 6 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑌 / 𝑥⦌𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))
16	13, 15	imbi12d 234	. . . . 5 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (([𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴) ↔ ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)))
17		ifeqeqx.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝑊)
18		nfcvd 2387	. . . . . . . . . . 11 ⊢ (𝑋 ∈ 𝑊 → Ⅎ𝑥𝐶)
19		ifeqeqx.1	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → 𝐴 = 𝐶)
20	18, 19	csbiegf 3185	. . . . . . . . . 10 ⊢ (𝑋 ∈ 𝑊 → ⦋𝑋 / 𝑥⦌𝐴 = 𝐶)
21	17, 20	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 = 𝐶)
22		ifeqeqx.5	. . . . . . . . 9 ⊢ (𝜑 → 𝑎 = 𝐶)
23	21, 22	eqtr4d 2270	. . . . . . . 8 ⊢ (𝜑 → ⦋𝑋 / 𝑥⦌𝐴 = 𝑎)
24	23	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝜓) → ⦋𝑋 / 𝑥⦌𝐴 = 𝑎)
25	24	eqcomd 2240	. . . . . 6 ⊢ ((𝜑 ∧ 𝜓) → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴)
26	25	a1d 22	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ([𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐴))
27		pm3.24 701	. . . . . . . . . 10 ⊢ ¬ (𝜓 ∧ ¬ 𝜓)
28		ifeqeqx.y	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
29		ifeqeqx.4	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑌 → (𝜒 ↔ 𝜓))
30	29	sbcieg 3078	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ 𝑉 → ([𝑌 / 𝑥]𝜒 ↔ 𝜓))
31	28, 30	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → ([𝑌 / 𝑥]𝜒 ↔ 𝜓))
32	31	anbi1d 465	. . . . . . . . . 10 ⊢ (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) ↔ (𝜓 ∧ ¬ 𝜓)))
33	27, 32	mtbiri 682	. . . . . . . . 9 ⊢ (𝜑 → ¬ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓))
34	33	pm2.21d 624	. . . . . . . 8 ⊢ (𝜑 → (([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴))
35	34	imp 124	. . . . . . 7 ⊢ ((𝜑 ∧ ([𝑌 / 𝑥]𝜒 ∧ ¬ 𝜓)) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴)
36	35	anass1rs 573	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝜓) ∧ [𝑌 / 𝑥]𝜒) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴)
37	36	ex 115	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝜓) → ([𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐴))
38		ifeqeqxdc.dc	. . . . 5 ⊢ (𝜑 → DECID 𝜓)
39	12, 16, 26, 37, 38	ifbothdadc 3660	. . . 4 ⊢ (𝜑 → ([if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))
40	4, 8, 39	sylc 62	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)
41		csbeq1a 3150	. . . . 5 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐴 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴)
42	41	eqeq2d 2246	. . . 4 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐴 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴))
43	42	biimprd 158	. . 3 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐴 → 𝑎 = 𝐴))
44	3, 40, 43	sylc 62	. 2 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜒) → 𝑎 = 𝐴)
45		simplr 529	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑥 = if(𝜓, 𝑋, 𝑌))
46		simpll 527	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝜑)
47		simpr 110	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ 𝜒)
48	6	notbid 673	. . . . . 6 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
49	48	biimpd 144	. . . . 5 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (¬ 𝜒 → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
50	45, 47, 49	sylc 62	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒)
51	9	notbid 673	. . . . . 6 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
52		csbeq1 3144	. . . . . . 7 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ⦋𝑋 / 𝑥⦌𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)
53	52	eqeq2d 2246	. . . . . 6 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑋 / 𝑥⦌𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))
54	51, 53	imbi12d 234	. . . . 5 ⊢ (𝑋 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)))
55	13	notbid 673	. . . . . 6 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (¬ [𝑌 / 𝑥]𝜒 ↔ ¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒))
56		csbeq1 3144	. . . . . . 7 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ⦋𝑌 / 𝑥⦌𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)
57	56	eqeq2d 2246	. . . . . 6 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋𝑌 / 𝑥⦌𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))
58	55, 57	imbi12d 234	. . . . 5 ⊢ (𝑌 = if(𝜓, 𝑋, 𝑌) → ((¬ [𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵) ↔ (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)))
59		ifeqeqx.3	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑋 → (𝜒 ↔ 𝜃))
60	59	sbcieg 3078	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ 𝑊 → ([𝑋 / 𝑥]𝜒 ↔ 𝜃))
61	17, 60	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → ([𝑋 / 𝑥]𝜒 ↔ 𝜃))
62	61	notbid 673	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 ↔ ¬ 𝜃))
63	62	biimpd 144	. . . . . . . . . 10 ⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜃))
64		ifeqeqx.6	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
65	64	ex 115	. . . . . . . . . 10 ⊢ (𝜑 → (𝜓 → 𝜃))
66	63, 65	nsyld 653	. . . . . . . . 9 ⊢ (𝜑 → (¬ [𝑋 / 𝑥]𝜒 → ¬ 𝜓))
67	66	anim2d 337	. . . . . . . 8 ⊢ (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → (𝜓 ∧ ¬ 𝜓)))
68	27, 67	mtoi 670	. . . . . . 7 ⊢ (𝜑 → ¬ (𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒))
69	68	pm2.21d 624	. . . . . 6 ⊢ (𝜑 → ((𝜓 ∧ ¬ [𝑋 / 𝑥]𝜒) → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵))
70	69	expdimp 259	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → (¬ [𝑋 / 𝑥]𝜒 → 𝑎 = ⦋𝑋 / 𝑥⦌𝐵))
71		nfcvd 2387	. . . . . . . . . 10 ⊢ (𝑌 ∈ 𝑉 → Ⅎ𝑥𝑎)
72		ifeqeqx.2	. . . . . . . . . 10 ⊢ (𝑥 = 𝑌 → 𝐵 = 𝑎)
73	71, 72	csbiegf 3185	. . . . . . . . 9 ⊢ (𝑌 ∈ 𝑉 → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎)
74	28, 73	syl 14	. . . . . . . 8 ⊢ (𝜑 → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎)
75	74	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝜓) → ⦋𝑌 / 𝑥⦌𝐵 = 𝑎)
76	75	eqcomd 2240	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵)
77	76	a1d 22	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝜓) → (¬ [𝑌 / 𝑥]𝜒 → 𝑎 = ⦋𝑌 / 𝑥⦌𝐵))
78	54, 58, 70, 77, 38	ifbothdadc 3660	. . . 4 ⊢ (𝜑 → (¬ [if(𝜓, 𝑋, 𝑌) / 𝑥]𝜒 → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))
79	46, 50, 78	sylc 62	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)
80		csbeq1a 3150	. . . . 5 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → 𝐵 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵)
81	80	eqeq2d 2246	. . . 4 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = 𝐵 ↔ 𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵))
82	81	biimprd 158	. . 3 ⊢ (𝑥 = if(𝜓, 𝑋, 𝑌) → (𝑎 = ⦋if(𝜓, 𝑋, 𝑌) / 𝑥⦌𝐵 → 𝑎 = 𝐵))
83	45, 79, 82	sylc 62	. 2 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜒) → 𝑎 = 𝐵)
84	64	adantlr 477	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → 𝜃)
85		simplr 529	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → 𝑥 = if(𝜓, 𝑋, 𝑌))
86		simpr 110	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → 𝜓)
87	86	iftrued 3633	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → if(𝜓, 𝑋, 𝑌) = 𝑋)
88	85, 87	eqtrd 2267	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → 𝑥 = 𝑋)
89	88, 59	syl 14	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → (𝜒 ↔ 𝜃))
90	84, 89	mpbird 167	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → 𝜒)
91	90	orcd 741	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → (𝜒 ∨ ¬ 𝜒))
92		df-dc 843	. . . 4 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
93	91, 92	sylibr 134	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ 𝜓) → DECID 𝜒)
94	38	ad2antrr 488	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜓) → DECID 𝜓)
95		simplr 529	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜓) → 𝑥 = if(𝜓, 𝑋, 𝑌))
96		simpr 110	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜓) → ¬ 𝜓)
97	96	iffalsed 3636	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜓) → if(𝜓, 𝑋, 𝑌) = 𝑌)
98	95, 97	eqtrd 2267	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜓) → 𝑥 = 𝑌)
99	98, 29	syl 14	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜓) → (𝜒 ↔ 𝜓))
100	99	dcbid 846	. . . 4 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜓) → (DECID 𝜒 ↔ DECID 𝜓))
101	94, 100	mpbird 167	. . 3 ⊢ (((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) ∧ ¬ 𝜓) → DECID 𝜒)
102		exmiddc 844	. . . . 5 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓))
103	38, 102	syl 14	. . . 4 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))
104	103	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → (𝜓 ∨ ¬ 𝜓))
105	93, 101, 104	mpjaodan 806	. 2 ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → DECID 𝜒)
106	1, 2, 44, 83, 105	ifbothdadc 3660	1 ⊢ ((𝜑 ∧ 𝑥 = if(𝜓, 𝑋, 𝑌)) → 𝑎 = if(𝜒, 𝐴, 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 716  DECID wdc 842   = wceq 1398   ∈ wcel 2205  [wsbc 3045  ⦋csb 3141  ifcif 3624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-sbc 3046  df-csb 3142  df-if 3625

This theorem is referenced by:  ballotfilemsf1o  13201