Theorem ifcldcd 3641

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 713  DECID wdc 839   = wceq 1395   ∈ wcel 2200  ifcif 3603

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-dc 840  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3604

This theorem is referenced by:  pw2f1odclem  7015  fimax2gtrilemstep  7083  nnnninf  7316  nnnninfeq  7318  fodjuf  7335  fodjum  7336  fodju0  7337  mkvprop  7348  nninfwlporlemd  7362  nninfwlporlem  7363  nninfwlpoimlemg  7365  nninfwlpoimlemginf  7366  xaddf  10069  xaddval  10070  nninfinf  10695  seqf1oglem1  10771  seqf1oglem2  10772  uzin2  11538  fsum3ser  11948  fsumsplit  11958  explecnv  12056  fprodsplitdc  12147  nninfctlemfo  12601  pcmpt2  12907  ennnfonelemp1  13017  opifismgmdc  13444  psr1clfi  14692  elply2  15449  ply1term  15457  plyaddlem1  15461  plyaddlem  15463  lgsval  15723  lgsfvalg  15724  lgsfcl2  15725  lgscllem  15726  lgsval2lem  15729  lgsneg  15743  lgsdilem  15746  lgsdir2  15752  lgsdir  15754  lgsdi  15756  lgsne0  15757  gausslemma2dlem1cl  15778  gausslemma2dlem4  15783  bj-charfundc  16339  2omap  16530  nnsf  16543  peano4nninf  16544  nninfsellemcl  16549  nninffeq  16558  dceqnconst  16600  dcapnconst  16601