Theorem ifcldadc 3600

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 3576	. . . 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 2282	. 2 |- ( ( ph /\ ps ) -> if ( ps , A , B ) e. C )
5		iffalse 3579	. . . 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 2282	. 2 |- ( ( ph /\ -. ps ) -> if ( ps , A , B ) e. C )
9		ifcldadc.dc	. . 3 |- ( ph -> DECID ps )
10		exmiddc 838	. . 3 |- (DECID ps -> ( ps \/ -. ps ) )
11	9, 10	syl 14	. 2 |- ( ph -> ( ps \/ -. ps ) )
12	4, 8, 11	mpjaodan 800	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 710  DECID wdc 836   = wceq 1373   e. wcel 2176   ifcif 3571

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 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-dc 837  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-if 3572

This theorem is referenced by:  updjudhf  7183  omp1eomlem  7198  difinfsnlem  7203  ctmlemr  7212  ctssdclemn0  7214  ctssdc  7217  enumctlemm  7218  xaddf  9968  xaddval  9969  iseqf1olemqcl  10646  iseqf1olemnab  10648  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  seq3f1oleml  10663  seq3f1o  10664  exp3val  10688  ccatcl  11052  swrdclg  11106  xrmaxiflemcl  11589  summodclem2a  11725  zsumdc  11728  fsum3  11731  isumss  11735  fsum3cvg2  11738  fsum3ser  11741  fsumcl2lem  11742  fsumadd  11750  sumsnf  11753  sumsplitdc  11776  fsummulc2  11792  isumlessdc  11840  cvgratz  11876  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  fprodmul  11935  prodsnf  11936  eucalgval2  12408  lcmval  12418  pcmpt  12699  ennnfonelemg  12807  mulgval  13491  mulgfng  13493  elplyd  15246  dvply1  15270  lgsval  15514  lgsfvalg  15515  lgsfcl2  15516  lgscllem  15517  lgsval2lem  15520  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  subctctexmid  15974