Theorem ifcldadc 3599

Description: Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.)

Hypotheses

Ref	Expression
ifcldadc.1	⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
ifcldadc.2	⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
ifcldadc.dc	⊢ (𝜑 → DECID 𝜓)

Assertion

Ref	Expression
ifcldadc	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifcldadc

Step	Hyp	Ref	Expression
1		iftrue 3575	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 277	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifcldadc.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2281	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 3578	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 277	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifcldadc.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2281	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9		ifcldadc.dc	. . 3 ⊢ (𝜑 → DECID 𝜓)
10		exmiddc 837	. . 3 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓))
11	9, 10	syl 14	. 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))
12	4, 8, 11	mpjaodan 799	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 709  DECID wdc 835   = wceq 1372   ∈ wcel 2175  ifcif 3570

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-dc 836  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-if 3571

This theorem is referenced by:  updjudhf  7180  omp1eomlem  7195  difinfsnlem  7200  ctmlemr  7209  ctssdclemn0  7211  ctssdc  7214  enumctlemm  7215  xaddf  9965  xaddval  9966  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemjpcl  10651  iseqf1olemqpcl  10652  seq3f1oleml  10659  seq3f1o  10660  exp3val  10684  ccatcl  11047  xrmaxiflemcl  11498  summodclem2a  11634  zsumdc  11637  fsum3  11640  isumss  11644  fsum3cvg2  11647  fsum3ser  11650  fsumcl2lem  11651  fsumadd  11659  sumsnf  11662  sumsplitdc  11685  fsummulc2  11701  isumlessdc  11749  cvgratz  11785  prodmodclem3  11828  prodmodclem2a  11829  zproddc  11832  fprodseq  11836  fprodmul  11844  prodsnf  11845  eucalgval2  12317  lcmval  12327  pcmpt  12608  ennnfonelemg  12716  mulgval  13400  mulgfng  13402  elplyd  15155  dvply1  15179  lgsval  15423  lgsfvalg  15424  lgsfcl2  15425  lgscllem  15426  lgsval2lem  15429  lgsdir  15454  lgsdilem2  15455  lgsdi  15456  lgsne0  15457  subctctexmid  15870