Theorem ifclda 4564

Description: Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
ifclda.1	⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
ifclda.2	⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
ifclda	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifclda

Step	Hyp	Ref	Expression
1		iftrue 4535	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 483	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2834	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4538	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 483	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2834	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 812	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  unxpdomlem3  9252  updjudhf  9926  acndom  10046  iunfictbso  10109  dfac12lem2  10139  ttukeylem6  10509  canthp1lem2  10648  xaddf  13203  xmulf  13251  ccatcl  14524  swrdcl  14595  ccatco  14786  lo1bdd2  15468  o1lo1  15481  sadadd2lem2  16391  sadcaddlem  16398  sadadd2lem  16400  sadadd3  16402  lcmfval  16558  iserodd  16768  prmreclem2  16850  prmreclem4  16852  prmreclem6  16854  prmrec  16855  vdwlem6  16919  mreexexd  17592  smndex2hbas  18797  symgextf  19285  pmtrf  19323  odfval  19400  cyggex2  19765  dprdfid  19887  dmdprdsplitlem  19907  sdrgacs  20417  cygznlem1  21122  cygznlem2a  21123  cygznlem3  21125  cygth  21127  fvmptnn04if  22351  chfacfisf  22356  chfacfisfcpmat  22357  ptpjpre2  23084  ptopn2  23088  ptpjopn  23116  iccpnfcnv  24460  xrhmeo  24462  cmetcaulem  24805  ovolunlem1a  25013  ovolunlem1  25014  ioorf  25090  mbfi1fseqlem3  25235  mbfi1flim  25241  itg2seq  25260  itg2splitlem  25266  itg2split  25267  iblss  25322  itgle  25327  itgeqa  25331  ibladdlem  25337  itgaddlem1  25340  iblabslem  25345  iblabs  25346  iblabsr  25347  iblmulc2  25348  itgmulc2lem1  25349  bddmulibl  25356  bddiblnc  25359  itggt0  25361  itgcn  25362  ellimc2  25394  limccnp  25408  limccnp2  25409  dvcobr  25463  lhop1  25531  elplyd  25716  coeeq2  25756  dvply1  25797  aalioulem3  25847  dvtaylp  25882  dvradcnv  25933  psercnlem1  25937  logcnlem2  26151  logcnlem3  26152  logcnlem4  26153  logtayllem  26167  logtayl  26168  cxpcl  26182  recxpcl  26183  leibpilem2  26446  leibpi  26447  rlimcnp2  26471  efrlim  26474  igamf  26555  igamcl  26556  pclogsum  26718  dchrelbasd  26742  lgsfcl2  26806  lgscllem  26807  lgsval2lem  26810  lgsne0  26838  2sqnn0  26941  dchrvmasumiflem2  27005  dchrisum0flblem1  27011  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntlemj  27106  padicabv  27133  crctcshwlkn0  29075  sgnsval  32320  gsummoncoe1fzo  32668  xrge0iifcnv  32913  xrge0iifhom  32917  pnfneige0  32931  esumpinfval  33071  sigaclfu2  33119  ballotlemsv  33508  ballotlemsdom  33510  signswmnd  33568  signsvvf  33590  signsvfn  33593  mrsubcv  34501  mrsubff  34503  mrsubrn  34504  mrsubccat  34509  gg-dvcobr  35176  unblimceq0lem  35382  ptrecube  36488  poimirlem24  36512  itg2addnclem2  36540  itg2gt0cn  36543  ibladdnclem  36544  itgaddnclem1  36546  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  itgmulc2nclem1  36554  itggt0cn  36558  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  areacirc  36581  cdleme27cl  39237  selvcllem5  41154  selvvvval  41157  dffltz  41376  cantnfub  42071  climsuse  44324  lptioo1  44348  icccncfext  44603  cncfiooicclem1  44609  iblsplit  44682  dirkerval2  44810  dirkerre  44811  fourierdlem9  44832  fourierdlem17  44840  fourierdlem43  44866  etransclem3  44953  etransclem7  44957  etransclem10  44960  etransclem21  44971  lincext1  47135