Theorem ifcldcd 3678

Description: Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.)

Hypotheses

Ref	Expression
ifcldcd.a	|- ( ph -> A e. C )
ifcldcd.b	|- ( ph -> B e. C )
ifcldcd.dc	|- ( ph -> DECID ps )

Assertion

Ref	Expression
ifcldcd	|- ( ph -> if ( ps , A , B ) e. C )

Proof of Theorem ifcldcd

Step	Hyp	Ref	Expression
1		iftrue 3645	. . . 4 |- ( ps -> if ( ps , A , B ) = A )
2	1	adantl 277	. . 3 |- ( ( ph /\ ps ) -> if ( ps , A , B ) = A )
3		ifcldcd.a	. . . 4 |- ( ph -> A e. C )
4	3	adantr 276	. . 3 |- ( ( ph /\ ps ) -> A e. C )
5	2, 4	eqeltrd 2315	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
6		iffalse 3648	. . . 4 |- ( -. ps -> if ( ps , A , B ) = B )
7	6	adantl 277	. . 3 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = B )
8		ifcldcd.b	. . . 4 |- ( ph -> B e. C )
9	8	adantr 276	. . 3 |- ( ( ph /\ -. ps ) -> B e. C )
10	7, 9	eqeltrd 2315	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
11		ifcldcd.dc	. . 3 |- ( ph -> DECID ps )
12		df-dc 847	. . 3 |- (DECID ps <-> ( ps \/ -. ps ) )
13	11, 12	sylib 122	. 2 |- ( ph -> ( ps \/ -. ps ) )
14	5, 10, 13	mpjaodan 810	1 |- ( ph -> if ( ps , A , B ) e. C )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 720  DECID wdc 846   = wceq 1402   e. wcel 2209   ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-dc 847  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-if 3639

This theorem is used by:  pw2f1odclem  7128  fimax2gtrilemstep  7199  snopfsuppdc  7293  2omap  7312  nnnninf  7460  nnnninfeq  7462  fodjuf  7479  fodjum  7480  fodju0  7481  mkvprop  7492  nninfwlporlemd  7506  nninfwlporlem  7507  nninfwlpoimlemg  7509  nninfwlpoimlemginf  7510  xaddf  10229  xaddval  10230  nninfinf  10863  seqf1oglem1  10939  seqf1oglem2  10940  uzin2  11736  fsum3ser  12147  fsumsplit  12157  explecnv  12255  fprodsplitdc  12346  nninfctlemfo  12800  pcmpt2  13106  ennnfonelemp1  13280  opifismgmdc  13674  psr1clfi  15062  elply2  15819  ply1term  15827  plyaddlem1  15831  plyaddlem  15833  lgsval  16106  lgsfvalg  16107  lgsfcl2  16108  lgscllem  16109  lgsval2lem  16112  lgsneg  16126  lgsdilem  16129  lgsdir2  16135  lgsdir  16137  lgsdi  16139  lgsne0  16140  gausslemma2dlem1cl  16161  gausslemma2dlem4  16166  eupth2lemsfi  16702  bj-charfundc  16817  nnsf  17023  peano4nninf  17024  nninfsellemcl  17029  nninffeq  17038  dceqnconst  17085  dcapnconst  17086