Theorem ifcldcd 3617

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 710  DECID wdc 836   = wceq 1373   ∈ wcel 2178  ifcif 3579

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 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-dc 837  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-if 3580

This theorem is referenced by:  pw2f1odclem  6956  fimax2gtrilemstep  7023  nnnninf  7254  nnnninfeq  7256  fodjuf  7273  fodjum  7274  fodju0  7275  mkvprop  7286  nninfwlporlemd  7300  nninfwlporlem  7301  nninfwlpoimlemg  7303  nninfwlpoimlemginf  7304  xaddf  10001  xaddval  10002  nninfinf  10625  seqf1oglem1  10701  seqf1oglem2  10702  uzin2  11413  fsum3ser  11823  fsumsplit  11833  explecnv  11931  fprodsplitdc  12022  nninfctlemfo  12476  pcmpt2  12782  ennnfonelemp1  12892  opifismgmdc  13318  psr1clfi  14565  elply2  15322  ply1term  15330  plyaddlem1  15334  plyaddlem  15336  lgsval  15596  lgsfvalg  15597  lgsfcl2  15598  lgscllem  15599  lgsval2lem  15602  lgsneg  15616  lgsdilem  15619  lgsdir2  15625  lgsdir  15627  lgsdi  15629  lgsne0  15630  gausslemma2dlem1cl  15651  gausslemma2dlem4  15656  bj-charfundc  15943  2omap  16132  nnsf  16144  peano4nninf  16145  nninfsellemcl  16150  nninffeq  16159  dceqnconst  16201  dcapnconst  16202