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

Theorem ifcldcd 3570
Description: Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.)
Hypotheses
Ref Expression
ifcldcd.a (𝜑𝐴𝐶)
ifcldcd.b (𝜑𝐵𝐶)
ifcldcd.dc (𝜑DECID 𝜓)
Assertion
Ref Expression
ifcldcd (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifcldcd
StepHypRef Expression
1 iftrue 3539 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 277 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifcldcd.a . . . 4 (𝜑𝐴𝐶)
43adantr 276 . . 3 ((𝜑𝜓) → 𝐴𝐶)
52, 4eqeltrd 2254 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
6 iffalse 3542 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
76adantl 277 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
8 ifcldcd.b . . . 4 (𝜑𝐵𝐶)
98adantr 276 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
107, 9eqeltrd 2254 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
11 ifcldcd.dc . . 3 (𝜑DECID 𝜓)
12 df-dc 835 . . 3 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
1311, 12sylib 122 . 2 (𝜑 → (𝜓 ∨ ¬ 𝜓))
145, 10, 13mpjaodan 798 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wo 708  DECID wdc 834   = wceq 1353  wcel 2148  ifcif 3534
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 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-dc 835  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-if 3535
This theorem is referenced by:  fimax2gtrilemstep  6899  nnnninf  7123  nnnninfeq  7125  fodjuf  7142  fodjum  7143  fodju0  7144  mkvprop  7155  nninfwlporlemd  7169  nninfwlporlem  7170  nninfwlpoimlemg  7172  nninfwlpoimlemginf  7173  xaddf  9842  xaddval  9843  uzin2  10991  fsum3ser  11400  fsumsplit  11410  explecnv  11508  fprodsplitdc  11599  pcmpt2  12336  ennnfonelemp1  12401  opifismgmdc  12744  lgsval  14298  lgsfvalg  14299  lgsfcl2  14300  lgscllem  14301  lgsval2lem  14304  lgsneg  14318  lgsdilem  14321  lgsdir2  14327  lgsdir  14329  lgsdi  14331  lgsne0  14332  bj-charfundc  14442  nnsf  14636  peano4nninf  14637  nninfsellemcl  14642  nninffeq  14651  dceqnconst  14689  dcapnconst  14690
  Copyright terms: Public domain W3C validator