Theorem ifcldadc 3600

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 3576	. . . 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 2282	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
5		iffalse 3579	. . . 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 2282	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
9		ifcldadc.dc	. . 3 |- ( ph -> DECID ps )
10		exmiddc 838	. . 3 |- (DECID ps -> ( ps \/ -. ps ) )
11	9, 10	syl 14	. 2 |- ( ph -> ( ps \/ -. ps ) )
12	4, 8, 11	mpjaodan 800	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 710  DECID wdc 836   = wceq 1373   e. wcel 2176   ifcif 3571

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 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-dc 837  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-if 3572

This theorem is referenced by:  updjudhf  7181  omp1eomlem  7196  difinfsnlem  7201  ctmlemr  7210  ctssdclemn0  7212  ctssdc  7215  enumctlemm  7216  xaddf  9966  xaddval  9967  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemjpcl  10653  iseqf1olemqpcl  10654  seq3f1oleml  10661  seq3f1o  10662  exp3val  10686  ccatcl  11049  swrdclg  11103  xrmaxiflemcl  11556  summodclem2a  11692  zsumdc  11695  fsum3  11698  isumss  11702  fsum3cvg2  11705  fsum3ser  11708  fsumcl2lem  11709  fsumadd  11717  sumsnf  11720  sumsplitdc  11743  fsummulc2  11759  isumlessdc  11807  cvgratz  11843  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  fprodmul  11902  prodsnf  11903  eucalgval2  12375  lcmval  12385  pcmpt  12666  ennnfonelemg  12774  mulgval  13458  mulgfng  13460  elplyd  15213  dvply1  15237  lgsval  15481  lgsfvalg  15482  lgsfcl2  15483  lgscllem  15484  lgsval2lem  15487  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  subctctexmid  15937