Theorem ifcldcd 3656

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 3623	. . . 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 2309	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
6		iffalse 3626	. . . 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 2309	. 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 2203   ifcif 3616

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 2214

This theorem depends on definitions:  df-bi 117  df-dc 843  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-if 3617

This theorem is referenced by:  pw2f1odclem  7078  fimax2gtrilemstep  7149  snopfsuppdc  7243  2omap  7260  nnnninf  7408  nnnninfeq  7410  fodjuf  7427  fodjum  7428  fodju0  7429  mkvprop  7440  nninfwlporlemd  7454  nninfwlporlem  7455  nninfwlpoimlemg  7457  nninfwlpoimlemginf  7458  xaddf  10163  xaddval  10164  nninfinf  10791  seqf1oglem1  10867  seqf1oglem2  10868  uzin2  11650  fsum3ser  12061  fsumsplit  12071  explecnv  12169  fprodsplitdc  12260  nninfctlemfo  12714  pcmpt2  13020  ennnfonelemp1  13131  opifismgmdc  13558  psr1clfi  14813  elply2  15570  ply1term  15578  plyaddlem1  15582  plyaddlem  15584  lgsval  15847  lgsfvalg  15848  lgsfcl2  15849  lgscllem  15850  lgsval2lem  15853  lgsneg  15867  lgsdilem  15870  lgsdir2  15876  lgsdir  15878  lgsdi  15880  lgsne0  15881  gausslemma2dlem1cl  15902  gausslemma2dlem4  15907  eupth2lemsfi  16443  bj-charfundc  16548  nnsf  16753  peano4nninf  16754  nninfsellemcl  16759  nninffeq  16768  dceqnconst  16815  dcapnconst  16816