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  7073  omp1eomlem  7088  difinfsnlem  7093  ctmlemr  7102  ctssdclemn0  7104  ctssdc  7107  enumctlemm  7108  xaddf  9838  xaddval  9839  iseqf1olemqcl  10479  iseqf1olemnab  10481  iseqf1olemjpcl  10488  iseqf1olemqpcl  10489  seq3f1oleml  10496  seq3f1o  10497  exp3val  10515  xrmaxiflemcl  11244  summodclem2a  11380  zsumdc  11383  fsum3  11386  isumss  11390  fsum3cvg2  11393  fsum3ser  11396  fsumcl2lem  11397  fsumadd  11405  sumsnf  11408  sumsplitdc  11431  fsummulc2  11447  isumlessdc  11495  cvgratz  11531  prodmodclem3  11574  prodmodclem2a  11575  zproddc  11578  fprodseq  11582  fprodmul  11590  prodsnf  11591  eucalgval2  12043  lcmval  12053  pcmpt  12331  ennnfonelemg  12394  mulgval  12914  mulgfng  12915  lgsval  14187  lgsfvalg  14188  lgsfcl2  14189  lgscllem  14190  lgsval2lem  14193  lgsdir  14218  lgsdilem2  14219  lgsdi  14220  lgsne0  14221  subctctexmid  14521