Theorem ifcldadc 3563

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 3539	. . . 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 2254	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
5		iffalse 3542	. . . 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 2254	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
9		ifcldadc.dc	. . 3 |- ( ph -> DECID ps )
10		exmiddc 836	. . 3 |- (DECID ps -> ( ps \/ -. ps ) )
11	9, 10	syl 14	. 2 |- ( ph -> ( ps \/ -. ps ) )
12	4, 8, 11	mpjaodan 798	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 708  DECID wdc 834   = wceq 1353   e. wcel 2148   ifcif 3534

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 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-dc 835  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-if 3535

This theorem is referenced by:  updjudhf  7077  omp1eomlem  7092  difinfsnlem  7097  ctmlemr  7106  ctssdclemn0  7108  ctssdc  7111  enumctlemm  7112  xaddf  9842  xaddval  9843  iseqf1olemqcl  10483  iseqf1olemnab  10485  iseqf1olemjpcl  10492  iseqf1olemqpcl  10493  seq3f1oleml  10500  seq3f1o  10501  exp3val  10519  xrmaxiflemcl  11248  summodclem2a  11384  zsumdc  11387  fsum3  11390  isumss  11394  fsum3cvg2  11397  fsum3ser  11400  fsumcl2lem  11401  fsumadd  11409  sumsnf  11412  sumsplitdc  11435  fsummulc2  11451  isumlessdc  11499  cvgratz  11535  prodmodclem3  11578  prodmodclem2a  11579  zproddc  11582  fprodseq  11586  fprodmul  11594  prodsnf  11595  eucalgval2  12047  lcmval  12057  pcmpt  12335  ennnfonelemg  12398  mulgval  12940  mulgfng  12941  lgsval  14298  lgsfvalg  14299  lgsfcl2  14300  lgscllem  14301  lgsval2lem  14304  lgsdir  14329  lgsdilem2  14330  lgsdi  14331  lgsne0  14332  subctctexmid  14632