Theorem ifcldadc 3670

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720  DECID wdc 846   = wceq 1402   ∈ wcel 2209  ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-dc 847  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  updjudhf  7420  omp1eomlem  7435  difinfsnlem  7440  ctmlemr  7449  ctssdclemn0  7451  ctssdc  7454  enumctlemm  7455  xaddf  10257  xaddval  10258  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  seq3f1oleml  10968  seq3f1o  10969  exp3val  10993  ccatcl  11377  swrdclg  11438  xrmaxiflemcl  12030  summodclem2a  12167  zsumdc  12170  fsum3  12173  isumss  12177  fsum3cvg2  12180  fsum3ser  12183  fsumcl2lem  12184  fsumadd  12192  sumsnf  12195  sumsplitdc  12218  fsummulc2  12234  isumlessdc  12282  cvgratz  12318  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodmul  12377  prodsnf  12378  eucalgval2  12850  lcmval  12860  pcmpt  13145  ballotfilemsv  13305  ballotfilemsdom  13307  ennnfonelemg  13346  mulgval  13978  mulgfng  13980  elplyd  15933  dvply1  15957  bposlem5  16276  lgsval  16289  lgsfvalg  16290  lgsfcl2  16291  lgscllem  16292  lgsval2lem  16295  lgsdir  16320  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  subctctexmid  17196