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 )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 720  DECID wdc 846   = wceq 1402   e. wcel 2209   ifcif 3638

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 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 theorem 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 referenced by:  pw2f1odclem  7127  fimax2gtrilemstep  7198  snopfsuppdc  7292  2omap  7311  nnnninf  7459  nnnninfeq  7461  fodjuf  7478  fodjum  7479  fodju0  7480  mkvprop  7491  nninfwlporlemd  7505  nninfwlporlem  7506  nninfwlpoimlemg  7508  nninfwlpoimlemginf  7509  xaddf  10228  xaddval  10229  nninfinf  10861  seqf1oglem1  10937  seqf1oglem2  10938  uzin2  11734  fsum3ser  12145  fsumsplit  12155  explecnv  12253  fprodsplitdc  12344  nninfctlemfo  12798  pcmpt2  13104  ennnfonelemp1  13278  opifismgmdc  13671  psr1clfi  15005  elply2  15762  ply1term  15770  plyaddlem1  15774  plyaddlem  15776  lgsval  16040  lgsfvalg  16041  lgsfcl2  16042  lgscllem  16043  lgsval2lem  16046  lgsneg  16060  lgsdilem  16063  lgsdir2  16069  lgsdir  16071  lgsdi  16073  lgsne0  16074  gausslemma2dlem1cl  16095  gausslemma2dlem4  16100  eupth2lemsfi  16636  bj-charfundc  16751  nnsf  16956  peano4nninf  16957  nninfsellemcl  16962  nninffeq  16971  dceqnconst  17018  dcapnconst  17019