Theorem ifcldadc 3670

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 3645	. . . 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 2315	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
5		iffalse 3648	. . . 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 2315	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
9		ifcldadc.dc	. . 3 |- ( ph -> DECID ps )
10		exmiddc 848	. . 3 |- (DECID ps -> ( ps \/ -. ps ) )
11	9, 10	syl 14	. 2 |- ( ph -> ( ps \/ -. ps ) )
12	4, 8, 11	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:  updjudhf  7419  omp1eomlem  7434  difinfsnlem  7439  ctmlemr  7448  ctssdclemn0  7450  ctssdc  7453  enumctlemm  7454  xaddf  10246  xaddval  10247  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  seq3f1oleml  10953  seq3f1o  10954  exp3val  10978  ccatcl  11361  swrdclg  11422  xrmaxiflemcl  12011  summodclem2a  12148  zsumdc  12151  fsum3  12154  isumss  12158  fsum3cvg2  12161  fsum3ser  12164  fsumcl2lem  12165  fsumadd  12173  sumsnf  12176  sumsplitdc  12199  fsummulc2  12215  isumlessdc  12263  cvgratz  12299  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodmul  12358  prodsnf  12359  eucalgval2  12831  lcmval  12841  pcmpt  13122  ballotfilemsv  13253  ballotfilemsdom  13255  ennnfonelemg  13294  mulgval  13925  mulgfng  13927  elplyd  15842  dvply1  15866  lgsval  16123  lgsfvalg  16124  lgsfcl2  16125  lgscllem  16126  lgsval2lem  16129  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  subctctexmid  17030