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  7425  omp1eomlem  7440  difinfsnlem  7445  ctmlemr  7454  ctssdclemn0  7456  ctssdc  7459  enumctlemm  7460  xaddf  10262  xaddval  10263  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  seq3f1oleml  10973  seq3f1o  10974  exp3val  10998  ccatcl  11382  swrdclg  11443  xrmaxiflemcl  12035  summodclem2a  12172  zsumdc  12175  fsum3  12178  isumss  12182  fsum3cvg2  12185  fsum3ser  12188  fsumcl2lem  12189  fsumadd  12197  sumsnf  12200  sumsplitdc  12223  fsummulc2  12239  isumlessdc  12287  cvgratz  12323  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodmul  12382  prodsnf  12383  eucalgval2  12855  lcmval  12865  pcmpt  13150  ballotfilemsv  13310  ballotfilemsdom  13312  ennnfonelemg  13351  mulgval  13983  mulgfng  13985  elplyd  15984  dvply1  16008  bposlem5  16332  lgsval  16345  lgsfvalg  16346  lgsfcl2  16347  lgscllem  16348  lgsval2lem  16351  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  subctctexmid  17252