Theorem ifcldcd 3561

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 3531	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 275	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifcldcd.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	3	adantr 274	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
5	2, 4	eqeltrd 2247	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
6		iffalse 3534	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
7	6	adantl 275	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
8		ifcldcd.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
9	8	adantr 274	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
10	7, 9	eqeltrd 2247	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
11		ifcldcd.dc	. . 3 ⊢ (𝜑 → DECID 𝜓)
12		df-dc 830	. . 3 ⊢ (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
13	11, 12	sylib 121	. 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))
14	5, 10, 13	mpjaodan 793	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 703  DECID wdc 829   = wceq 1348   ∈ wcel 2141  ifcif 3526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-dc 830  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-if 3527

This theorem is referenced by:  fimax2gtrilemstep  6878  nnnninf  7102  nnnninfeq  7104  fodjuf  7121  fodjum  7122  fodju0  7123  mkvprop  7134  nninfwlporlemd  7148  nninfwlporlem  7149  nninfwlpoimlemg  7151  nninfwlpoimlemginf  7152  xaddf  9801  xaddval  9802  uzin2  10951  fsum3ser  11360  fsumsplit  11370  explecnv  11468  fprodsplitdc  11559  pcmpt2  12296  ennnfonelemp1  12361  opifismgmdc  12625  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgscllem  13702  lgsval2lem  13705  lgsneg  13719  lgsdilem  13722  lgsdir2  13728  lgsdir  13730  lgsdi  13732  lgsne0  13733  bj-charfundc  13843  nnsf  14038  peano4nninf  14039  nninfsellemcl  14044  nninffeq  14053  dceqnconst  14091  dcapnconst  14092