Theorem ifcldadc 3639

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 3614	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 277	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifcldadc.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2308	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 3617	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 277	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifcldadc.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2308	. 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 2202  ifcif 3607

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 2213

This theorem depends on definitions:  df-bi 117  df-dc 843  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-if 3608

This theorem is referenced by:  updjudhf  7321  omp1eomlem  7336  difinfsnlem  7341  ctmlemr  7350  ctssdclemn0  7352  ctssdc  7355  enumctlemm  7356  xaddf  10123  xaddval  10124  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  seq3f1oleml  10824  seq3f1o  10825  exp3val  10849  ccatcl  11219  swrdclg  11280  xrmaxiflemcl  11868  summodclem2a  12005  zsumdc  12008  fsum3  12011  isumss  12015  fsum3cvg2  12018  fsum3ser  12021  fsumcl2lem  12022  fsumadd  12030  sumsnf  12033  sumsplitdc  12056  fsummulc2  12072  isumlessdc  12120  cvgratz  12156  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodmul  12215  prodsnf  12216  eucalgval2  12688  lcmval  12698  pcmpt  12979  ennnfonelemg  13087  mulgval  13772  mulgfng  13774  elplyd  15535  dvply1  15559  lgsval  15806  lgsfvalg  15807  lgsfcl2  15808  lgscllem  15809  lgsval2lem  15812  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  subctctexmid  16705