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  7262  omp1eomlem  7277  difinfsnlem  7282  ctmlemr  7291  ctssdclemn0  7293  ctssdc  7296  enumctlemm  7297  xaddf  10057  xaddval  10058  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  seq3f1oleml  10755  seq3f1o  10756  exp3val  10780  ccatcl  11146  swrdclg  11203  xrmaxiflemcl  11777  summodclem2a  11913  zsumdc  11916  fsum3  11919  isumss  11923  fsum3cvg2  11926  fsum3ser  11929  fsumcl2lem  11930  fsumadd  11938  sumsnf  11941  sumsplitdc  11964  fsummulc2  11980  isumlessdc  12028  cvgratz  12064  prodmodclem3  12107  prodmodclem2a  12108  zproddc  12111  fprodseq  12115  fprodmul  12123  prodsnf  12124  eucalgval2  12596  lcmval  12606  pcmpt  12887  ennnfonelemg  12995  mulgval  13680  mulgfng  13682  elplyd  15436  dvply1  15460  lgsval  15704  lgsfvalg  15705  lgsfcl2  15706  lgscllem  15707  lgsval2lem  15710  lgsdir  15735  lgsdilem2  15736  lgsdi  15737  lgsne0  15738  subctctexmid  16479