ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ifcldadc GIF version

Theorem ifcldadc 3554
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
StepHypRef Expression
1 iftrue 3530 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 275 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifcldadc.1 . . 3 ((𝜑𝜓) → 𝐴𝐶)
42, 3eqeltrd 2247 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5 iffalse 3533 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 275 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifcldadc.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
86, 7eqeltrd 2247 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9 ifcldadc.dc . . 3 (𝜑DECID 𝜓)
10 exmiddc 831 . . 3 (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓))
119, 10syl 14 . 2 (𝜑 → (𝜓 ∨ ¬ 𝜓))
124, 8, 11mpjaodan 793 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 703  DECID wdc 829   = wceq 1348  wcel 2141  ifcif 3525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-dc 830  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-if 3526
This theorem is referenced by:  updjudhf  7052  omp1eomlem  7067  difinfsnlem  7072  ctmlemr  7081  ctssdclemn0  7083  ctssdc  7086  enumctlemm  7087  xaddf  9788  xaddval  9789  iseqf1olemqcl  10429  iseqf1olemnab  10431  iseqf1olemjpcl  10438  iseqf1olemqpcl  10439  seq3f1oleml  10446  seq3f1o  10447  exp3val  10465  xrmaxiflemcl  11195  summodclem2a  11331  zsumdc  11334  fsum3  11337  isumss  11341  fsum3cvg2  11344  fsum3ser  11347  fsumcl2lem  11348  fsumadd  11356  sumsnf  11359  sumsplitdc  11382  fsummulc2  11398  isumlessdc  11446  cvgratz  11482  prodmodclem3  11525  prodmodclem2a  11526  zproddc  11529  fprodseq  11533  fprodmul  11541  prodsnf  11542  eucalgval2  11994  lcmval  12004  pcmpt  12282  ennnfonelemg  12345  lgsval  13658  lgsfvalg  13659  lgsfcl2  13660  lgscllem  13661  lgsval2lem  13664  lgsdir  13689  lgsdilem2  13690  lgsdi  13691  lgsne0  13692  subctctexmid  13994
  Copyright terms: Public domain W3C validator