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

Theorem ifcldadc 3555
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 3531 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 275 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifcldadc.1 . . 3 ((𝜑𝜓) → 𝐴𝐶)
42, 3eqeltrd 2247 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5 iffalse 3534 . . . 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 3526
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 3527
This theorem is referenced by:  updjudhf  7056  omp1eomlem  7071  difinfsnlem  7076  ctmlemr  7085  ctssdclemn0  7087  ctssdc  7090  enumctlemm  7091  xaddf  9801  xaddval  9802  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemjpcl  10451  iseqf1olemqpcl  10452  seq3f1oleml  10459  seq3f1o  10460  exp3val  10478  xrmaxiflemcl  11208  summodclem2a  11344  zsumdc  11347  fsum3  11350  isumss  11354  fsum3cvg2  11357  fsum3ser  11360  fsumcl2lem  11361  fsumadd  11369  sumsnf  11372  sumsplitdc  11395  fsummulc2  11411  isumlessdc  11459  cvgratz  11495  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodmul  11554  prodsnf  11555  eucalgval2  12007  lcmval  12017  pcmpt  12295  ennnfonelemg  12358  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgscllem  13702  lgsval2lem  13705  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  subctctexmid  14034
  Copyright terms: Public domain W3C validator