Theorem ifcldadc 3656

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 3631	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 277	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifcldadc.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2311	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 3634	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 277	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifcldadc.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2311	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9		ifcldadc.dc	. . 3 ⊢ (𝜑 → DECID 𝜓)
10		exmiddc 844	. . 3 ⊢ (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓))
11	9, 10	syl 14	. 2 ⊢ (𝜑 → (𝜓 ∨ ¬ 𝜓))
12	4, 8, 11	mpjaodan 806	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 716  DECID wdc 842   = wceq 1398   ∈ wcel 2205  ifcif 3624

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-dc 843  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3625

This theorem is referenced by:  updjudhf  7383  omp1eomlem  7398  difinfsnlem  7403  ctmlemr  7412  ctssdclemn0  7414  ctssdc  7417  enumctlemm  7418  xaddf  10196  xaddval  10197  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seq3f1oleml  10902  seq3f1o  10903  exp3val  10927  ccatcl  11306  swrdclg  11367  xrmaxiflemcl  11955  summodclem2a  12092  zsumdc  12095  fsum3  12098  isumss  12102  fsum3cvg2  12105  fsum3ser  12108  fsumcl2lem  12109  fsumadd  12117  sumsnf  12120  sumsplitdc  12143  fsummulc2  12159  isumlessdc  12207  cvgratz  12243  prodmodclem3  12286  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodmul  12302  prodsnf  12303  eucalgval2  12775  lcmval  12785  pcmpt  13066  ballotfilemsv  13197  ballotfilemsdom  13199  ennnfonelemg  13238  mulgval  13875  mulgfng  13877  elplyd  15732  dvply1  15756  lgsval  16003  lgsfvalg  16004  lgsfcl2  16005  lgscllem  16006  lgsval2lem  16009  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  subctctexmid  16900