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

Theorem ifcldcd 3477
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 3449 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 275 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifcldcd.a . . . 4 (𝜑𝐴𝐶)
43adantr 274 . . 3 ((𝜑𝜓) → 𝐴𝐶)
52, 4eqeltrd 2194 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
6 iffalse 3452 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
76adantl 275 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
8 ifcldcd.b . . . 4 (𝜑𝐵𝐶)
98adantr 274 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
107, 9eqeltrd 2194 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
11 ifcldcd.dc . . 3 (𝜑DECID 𝜓)
12 df-dc 805 . . 3 (DECID 𝜓 ↔ (𝜓 ∨ ¬ 𝜓))
1311, 12sylib 121 . 2 (𝜑 → (𝜓 ∨ ¬ 𝜓))
145, 10, 13mpjaodan 772 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 682  DECID wdc 804   = wceq 1316  wcel 1465  ifcif 3444
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 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-dc 805  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-if 3445
This theorem is referenced by:  fimax2gtrilemstep  6762  fodjuf  6985  fodjum  6986  fodju0  6987  nnnninf  6991  mkvprop  7000  xaddf  9595  xaddval  9596  uzin2  10727  fsum3ser  11134  fsumsplit  11144  explecnv  11242  ennnfonelemp1  11846  nnsf  13126  peano4nninf  13127  nninfalllemn  13129  nninfsellemcl  13134  nninffeq  13143
  Copyright terms: Public domain W3C validator