Theorem ifcldcd 3660

Description: Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.)

Hypotheses

Ref	Expression
ifcldcd.a	⊢ (𝜑 → 𝐴 ∈ 𝐶)
ifcldcd.b	⊢ (𝜑 → 𝐵 ∈ 𝐶)
ifcldcd.dc	⊢ (𝜑 → DECID 𝜓)

Assertion

Ref	Expression
ifcldcd	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifcldcd

Step	Hyp	Ref	Expression
1		iftrue 3627	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 277	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifcldcd.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	3	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
5	2, 4	eqeltrd 2309	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
6		iffalse 3630	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
7	6	adantl 277	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
8		ifcldcd.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
9	8	adantr 276	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
10	7, 9	eqeltrd 2309	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
11		ifcldcd.dc	. . 3 ⊢ (𝜑 → DECID 𝜓)
12		df-dc 843	. . 3 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
13	11, 12	sylib 122	. 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))
14	5, 10, 13	mpjaodan 806	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 716  DECID wdc 842   = wceq 1398   ∈ wcel 2203  ifcif 3620

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-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-dc 843  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-if 3621

This theorem is referenced by:  pw2f1odclem  7087  fimax2gtrilemstep  7158  snopfsuppdc  7252  2omap  7269  nnnninf  7417  nnnninfeq  7419  fodjuf  7436  fodjum  7437  fodju0  7438  mkvprop  7449  nninfwlporlemd  7463  nninfwlporlem  7464  nninfwlpoimlemg  7466  nninfwlpoimlemginf  7467  xaddf  10177  xaddval  10178  nninfinf  10805  seqf1oglem1  10881  seqf1oglem2  10882  uzin2  11672  fsum3ser  12083  fsumsplit  12093  explecnv  12191  fprodsplitdc  12282  nninfctlemfo  12736  pcmpt2  13042  ennnfonelemp1  13157  opifismgmdc  13584  psr1clfi  14843  elply2  15600  ply1term  15608  plyaddlem1  15612  plyaddlem  15614  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgscllem  15880  lgsval2lem  15883  lgsneg  15897  lgsdilem  15900  lgsdir2  15906  lgsdir  15908  lgsdi  15910  lgsne0  15911  gausslemma2dlem1cl  15932  gausslemma2dlem4  15937  eupth2lemsfi  16473  bj-charfundc  16578  nnsf  16783  peano4nninf  16784  nninfsellemcl  16789  nninffeq  16798  dceqnconst  16846  dcapnconst  16847