Theorem ifcldadc 3591

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 3567	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 277	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifcldadc.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2273	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 3570	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 277	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifcldadc.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2273	. 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 1364   ∈ wcel 2167  ifcif 3562

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-dc 836  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-if 3563

This theorem is referenced by:  updjudhf  7147  omp1eomlem  7162  difinfsnlem  7167  ctmlemr  7176  ctssdclemn0  7178  ctssdc  7181  enumctlemm  7182  xaddf  9922  xaddval  9923  iseqf1olemqcl  10594  iseqf1olemnab  10596  iseqf1olemjpcl  10603  iseqf1olemqpcl  10604  seq3f1oleml  10611  seq3f1o  10612  exp3val  10636  xrmaxiflemcl  11413  summodclem2a  11549  zsumdc  11552  fsum3  11555  isumss  11559  fsum3cvg2  11562  fsum3ser  11565  fsumcl2lem  11566  fsumadd  11574  sumsnf  11577  sumsplitdc  11600  fsummulc2  11616  isumlessdc  11664  cvgratz  11700  prodmodclem3  11743  prodmodclem2a  11744  zproddc  11747  fprodseq  11751  fprodmul  11759  prodsnf  11760  eucalgval2  12232  lcmval  12242  pcmpt  12523  ennnfonelemg  12631  mulgval  13278  mulgfng  13280  elplyd  15003  dvply1  15027  lgsval  15271  lgsfvalg  15272  lgsfcl2  15273  lgscllem  15274  lgsval2lem  15277  lgsdir  15302  lgsdilem2  15303  lgsdi  15304  lgsne0  15305  subctctexmid  15673