Theorem ifcldadc 3632

Description: Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.)

Hypotheses

Ref	Expression
ifcldadc.1	|- ( ( ph /\ ps ) -> A e. C )
ifcldadc.2	|- ( ( ph /\ -. ps ) -> B e. C )
ifcldadc.dc	|- ( ph -> DECID ps )

Assertion

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

Proof of Theorem ifcldadc

Step	Hyp	Ref	Expression
1		iftrue 3607	. . . 4 |- ( ps -> if ( ps , A , B ) = A )
2	1	adantl 277	. . 3 |- ( ( ph /\ ps ) -> if ( ps , A , B ) = A )
3		ifcldadc.1	. . 3 |- ( ( ph /\ ps ) -> A e. C )
4	2, 3	eqeltrd 2306	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
5		iffalse 3610	. . . 4 |- ( -. ps -> if ( ps , A , B ) = B )
6	5	adantl 277	. . 3 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) = B )
7		ifcldadc.2	. . 3 |- ( ( ph /\ -. ps ) -> B e. C )
8	6, 7	eqeltrd 2306	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
9		ifcldadc.dc	. . 3 |- ( ph -> DECID ps )
10		exmiddc 841	. . 3 |- (DECID ps -> ( ps \/ -. ps ) )
11	9, 10	syl 14	. 2 |- ( ph -> ( ps \/ -. ps ) )
12	4, 8, 11	mpjaodan 803	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 713  DECID wdc 839   = wceq 1395   e. wcel 2200   ifcif 3602

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 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-dc 840  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-if 3603

This theorem is referenced by:  updjudhf  7257  omp1eomlem  7272  difinfsnlem  7277  ctmlemr  7286  ctssdclemn0  7288  ctssdc  7291  enumctlemm  7292  xaddf  10052  xaddval  10053  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  seq3f1oleml  10750  seq3f1o  10751  exp3val  10775  ccatcl  11141  swrdclg  11198  xrmaxiflemcl  11772  summodclem2a  11908  zsumdc  11911  fsum3  11914  isumss  11918  fsum3cvg2  11921  fsum3ser  11924  fsumcl2lem  11925  fsumadd  11933  sumsnf  11936  sumsplitdc  11959  fsummulc2  11975  isumlessdc  12023  cvgratz  12059  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  fprodmul  12118  prodsnf  12119  eucalgval2  12591  lcmval  12601  pcmpt  12882  ennnfonelemg  12990  mulgval  13675  mulgfng  13677  elplyd  15431  dvply1  15455  lgsval  15699  lgsfvalg  15700  lgsfcl2  15701  lgscllem  15702  lgsval2lem  15705  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  subctctexmid  16453