Theorem ifcldcd 3678

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 3645	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 277	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifcldcd.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	3	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
5	2, 4	eqeltrd 2315	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
6		iffalse 3648	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
7	6	adantl 277	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
8		ifcldcd.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
9	8	adantr 276	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
10	7, 9	eqeltrd 2315	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
11		ifcldcd.dc	. . 3 ⊢ (𝜑 → DECID 𝜓)
12		df-dc 847	. . 3 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
13	11, 12	sylib 122	. 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))
14	5, 10, 13	mpjaodan 810	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720  DECID wdc 846   = wceq 1402   ∈ wcel 2209  ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-dc 847  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  ifprdc  3819  pw2f1odclem  7134  fimax2gtrilemstep  7205  snopfsuppdc  7299  2omap  7318  nnnninf  7466  nnnninfeq  7468  fodjuf  7485  fodjum  7486  fodju0  7487  mkvprop  7498  nninfwlporlemd  7512  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  xaddf  10256  xaddval  10257  nninfinf  10893  seqf1oglem1  10969  seqf1oglem2  10970  uzin2  11767  fsum3ser  12180  fsumsplit  12190  explecnv  12288  fprodsplitdc  12379  nninfctlemfo  12833  pcmpt2  13143  ennnfonelemp1  13346  opifismgmdc  13740  psr1clfi  15128  elply2  15885  ply1term  15893  plyaddlem1  15897  plyaddlem  15899  bposlem1  16209  lgsval  16221  lgsfvalg  16222  lgsfcl2  16223  lgscllem  16224  lgsval2lem  16227  lgsneg  16241  lgsdilem  16244  lgsdir2  16250  lgsdir  16252  lgsdi  16254  lgsne0  16255  gausslemma2dlem1cl  16276  gausslemma2dlem4  16281  eupth2lemsfi  16817  bj-charfundc  16932  nnsf  17146  peano4nninf  17147  nninfsellemcl  17152  nninffeq  17161  dceqnconst  17208  dcapnconst  17209