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  7246  omp1eomlem  7261  difinfsnlem  7266  ctmlemr  7275  ctssdclemn0  7277  ctssdc  7280  enumctlemm  7281  xaddf  10040  xaddval  10041  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  seq3f1oleml  10738  seq3f1o  10739  exp3val  10763  ccatcl  11128  swrdclg  11182  xrmaxiflemcl  11756  summodclem2a  11892  zsumdc  11895  fsum3  11898  isumss  11902  fsum3cvg2  11905  fsum3ser  11908  fsumcl2lem  11909  fsumadd  11917  sumsnf  11920  sumsplitdc  11943  fsummulc2  11959  isumlessdc  12007  cvgratz  12043  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  fprodmul  12102  prodsnf  12103  eucalgval2  12575  lcmval  12585  pcmpt  12866  ennnfonelemg  12974  mulgval  13659  mulgfng  13661  elplyd  15415  dvply1  15439  lgsval  15683  lgsfvalg  15684  lgsfcl2  15685  lgscllem  15686  lgsval2lem  15689  lgsdir  15714  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  subctctexmid  16366