Theorem ifcldcd 3662

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 3629	. . . 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 2311	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
6		iffalse 3632	. . . 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 2311	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
11		ifcldcd.dc	. . 3 |- ( ph -> DECID ps )
12		df-dc 843	. . 3 |- (DECID ps <-> ( ps \/ -. ps ) )
13	11, 12	sylib 122	. 2 |- ( ph -> ( ps \/ -. ps ) )
14	5, 10, 13	mpjaodan 806	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 716  DECID wdc 842   = wceq 1398   e. wcel 2205   ifcif 3622

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 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-dc 843  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-if 3623

This theorem is referenced by:  pw2f1odclem  7089  fimax2gtrilemstep  7160  snopfsuppdc  7254  2omap  7271  nnnninf  7419  nnnninfeq  7421  fodjuf  7438  fodjum  7439  fodju0  7440  mkvprop  7451  nninfwlporlemd  7465  nninfwlporlem  7466  nninfwlpoimlemg  7468  nninfwlpoimlemginf  7469  xaddf  10180  xaddval  10181  nninfinf  10809  seqf1oglem1  10885  seqf1oglem2  10886  uzin2  11676  fsum3ser  12087  fsumsplit  12097  explecnv  12195  fprodsplitdc  12286  nninfctlemfo  12740  pcmpt2  13046  ennnfonelemp1  13174  opifismgmdc  13601  psr1clfi  14860  elply2  15617  ply1term  15625  plyaddlem1  15629  plyaddlem  15631  lgsval  15894  lgsfvalg  15895  lgsfcl2  15896  lgscllem  15897  lgsval2lem  15900  lgsneg  15914  lgsdilem  15917  lgsdir2  15923  lgsdir  15925  lgsdi  15927  lgsne0  15928  gausslemma2dlem1cl  15949  gausslemma2dlem4  15954  eupth2lemsfi  16490  bj-charfundc  16595  nnsf  16800  peano4nninf  16801  nninfsellemcl  16806  nninffeq  16815  dceqnconst  16863  dcapnconst  16864