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

Theorem ifcldcd 3572
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 3541 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 277 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifcldcd.a . . . 4 (𝜑𝐴𝐶)
43adantr 276 . . 3 ((𝜑𝜓) → 𝐴𝐶)
52, 4eqeltrd 2254 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
6 iffalse 3544 . . . 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 3536
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 3537
This theorem is referenced by:  fimax2gtrilemstep  6902  nnnninf  7126  nnnninfeq  7128  fodjuf  7145  fodjum  7146  fodju0  7147  mkvprop  7158  nninfwlporlemd  7172  nninfwlporlem  7173  nninfwlpoimlemg  7175  nninfwlpoimlemginf  7176  xaddf  9846  xaddval  9847  uzin2  10998  fsum3ser  11407  fsumsplit  11417  explecnv  11515  fprodsplitdc  11606  pcmpt2  12344  ennnfonelemp1  12409  opifismgmdc  12795  lgsval  14490  lgsfvalg  14491  lgsfcl2  14492  lgscllem  14493  lgsval2lem  14496  lgsneg  14510  lgsdilem  14513  lgsdir2  14519  lgsdir  14521  lgsdi  14523  lgsne0  14524  bj-charfundc  14645  nnsf  14839  peano4nninf  14840  nninfsellemcl  14845  nninffeq  14854  dceqnconst  14893  dcapnconst  14894
  Copyright terms: Public domain W3C validator