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

Theorem ifcldadc 3440
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 3418 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 272 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifcldadc.1 . . 3 ((𝜑𝜓) → 𝐴𝐶)
42, 3eqeltrd 2171 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5 iffalse 3421 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 272 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifcldadc.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
86, 7eqeltrd 2171 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9 ifcldadc.dc . . 3 (𝜑DECID 𝜓)
10 exmiddc 785 . . 3 (DECID 𝜓 → (𝜓 ∨ ¬ 𝜓))
119, 10syl 14 . 2 (𝜑 → (𝜓 ∨ ¬ 𝜓))
124, 8, 11mpjaodan 750 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wo 667  DECID wdc 783   = wceq 1296  wcel 1445  ifcif 3413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-dc 784  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-if 3414
This theorem is referenced by:  updjudhf  6850  ctmlemr  6870  enumctlemm  6872  xaddf  9410  xaddval  9411  iseqf1olemqcl  10036  iseqf1olemnab  10038  iseqf1olemjpcl  10045  iseqf1olemqpcl  10046  seq3f1oleml  10053  seq3f1o  10054  exp3val  10072  xrmaxiflemcl  10788  summodclem2a  10924  zsumdc  10927  fsum3  10930  isumss  10934  fsum3cvg2  10937  fsum3ser  10940  fsumcl2lem  10941  fsumadd  10949  sumsnf  10952  sumsplitdc  10975  fsummulc2  10991  isumlessdc  11039  cvgratz  11075  eucalgval2  11462  lcmval  11472
  Copyright terms: Public domain W3C validator