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:  ifprdc  3819  pw2f1odclem  7138  fimax2gtrilemstep  7209  snopfsuppdc  7304  2omap  7324  nnnninf  7472  nnnninfeq  7474  fodjuf  7491  fodjum  7492  fodju0  7493  mkvprop  7504  nninfwlporlemd  7518  nninfwlporlem  7519  nninfwlpoimlemg  7521  nninfwlpoimlemginf  7522  xaddf  10263  xaddval  10264  nninfinf  10901  seqf1oglem1  10977  seqf1oglem2  10978  uzin2  11775  fsum3ser  12189  fsumsplit  12199  explecnv  12297  fprodsplitdc  12388  nninfctlemfo  12842  pcmpt2  13152  ennnfonelemp1  13355  opifismgmdc  13750  psr1clfi  15198  elply2  15961  ply1term  15969  plyaddlem1  15973  plyaddlem  15975  prmorcht  16282  chtublem  16295  bposlem1  16311  lgsval  16328  lgsfvalg  16329  lgsfcl2  16330  lgscllem  16331  lgsval2lem  16334  lgsneg  16348  lgsdilem  16351  lgsdir2  16357  lgsdir  16359  lgsdi  16361  lgsne0  16362  gausslemma2dlem1cl  16383  gausslemma2dlem4  16388  eupth2lemsfi  16924  bj-charfundc  17039  nnsf  17254  peano4nninf  17255  nninfsellemcl  17260  nninffeq  17269  dceqnconst  17317  dcapnconst  17318