Theorem ifcldcd 3643

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 715  DECID wdc 841   = wceq 1397   ∈ wcel 2202  ifcif 3605

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-dc 842  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3606

This theorem is referenced by:  pw2f1odclem  7019  fimax2gtrilemstep  7089  nnnninf  7324  nnnninfeq  7326  fodjuf  7343  fodjum  7344  fodju0  7345  mkvprop  7356  nninfwlporlemd  7370  nninfwlporlem  7371  nninfwlpoimlemg  7373  nninfwlpoimlemginf  7374  xaddf  10078  xaddval  10079  nninfinf  10704  seqf1oglem1  10780  seqf1oglem2  10781  uzin2  11547  fsum3ser  11957  fsumsplit  11967  explecnv  12065  fprodsplitdc  12156  nninfctlemfo  12610  pcmpt2  12916  ennnfonelemp1  13026  opifismgmdc  13453  psr1clfi  14701  elply2  15458  ply1term  15466  plyaddlem1  15470  plyaddlem  15472  lgsval  15732  lgsfvalg  15733  lgsfcl2  15734  lgscllem  15735  lgsval2lem  15738  lgsneg  15752  lgsdilem  15755  lgsdir2  15761  lgsdir  15763  lgsdi  15765  lgsne0  15766  gausslemma2dlem1cl  15787  gausslemma2dlem4  15792  bj-charfundc  16403  2omap  16594  nnsf  16607  peano4nninf  16608  nninfsellemcl  16613  nninffeq  16622  dceqnconst  16664  dcapnconst  16665