Theorem ifclda 4490

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 4460	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2839	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4463	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 482	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2839	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 818	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ifcif 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-if 4455

This theorem is referenced by:  unxpdomlem3  9158  updjudhf  9846  acndom  9964  iunfictbso  10027  dfac12lem2  10058  ttukeylem6  10427  canthp1lem2  10567  xaddf  13167  xmulf  13215  ccatcl  14527  swrdcl  14599  ccatco  14788  lo1bdd2  15477  o1lo1  15490  sadadd2lem2  16410  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  lcmfval  16581  iserodd  16797  prmreclem2  16879  prmreclem4  16881  prmreclem6  16883  prmrec  16884  vdwlem6  16948  mreexexd  17605  smndex2hbas  18878  symgextf  19383  pmtrf  19421  odfval  19498  cyggex2  19863  dprdfid  19985  dmdprdsplitlem  20005  sdrgacs  20773  cygznlem1  21541  cygznlem2a  21542  cygznlem3  21544  cygth  21546  selvcllem5  22115  selvvvval  22118  fvmptnn04if  22832  chfacfisf  22837  chfacfisfcpmat  22838  ptpjpre2  23563  ptopn2  23567  ptpjopn  23595  iccpnfcnv  24929  xrhmeo  24931  cmetcaulem  25273  ovolunlem1a  25481  ovolunlem1  25482  ioorf  25558  mbfi1fseqlem3  25702  mbfi1flim  25708  itg2seq  25727  itg2splitlem  25733  itg2split  25734  iblss  25790  itgle  25795  itgeqa  25799  ibladdlem  25805  itgaddlem1  25808  iblabslem  25813  iblabs  25814  iblabsr  25815  iblmulc2  25816  itgmulc2lem1  25817  bddmulibl  25824  bddiblnc  25827  itggt0  25829  itgcn  25830  ellimc2  25862  limccnp  25876  limccnp2  25877  dvcobr  25931  lhop1  25999  elplyd  26185  coeeq2  26225  dvply1  26268  aalioulem3  26318  dvtaylp  26353  dvradcnv  26404  psercnlem1  26408  logcnlem2  26625  logcnlem3  26626  logcnlem4  26627  logtayllem  26641  logtayl  26642  cxpcl  26656  recxpcl  26657  leibpilem2  26923  leibpi  26924  rlimcnp2  26948  efrlim  26951  igamf  27032  igamcl  27033  pclogsum  27196  dchrelbasd  27220  lgsfcl2  27284  lgscllem  27285  lgsval2lem  27288  lgsne0  27316  2sqnn0  27419  dchrvmasumiflem2  27483  dchrisum0flblem1  27489  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntlemj  27584  padicabv  27611  crctcshwlkn0  29907  ccatws1f1o  33030  sgnsval  33242  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  gsummoncoe1fzo  33680  selvascl  33701  fldextrspunlsp  33858  extdgfialglem2  33877  xrge0iifcnv  34117  xrge0iifhom  34121  pnfneige0  34135  esumpinfval  34257  sigaclfu2  34305  ballotlemsv  34694  ballotlemsdom  34696  signswmnd  34741  signsvvf  34763  signsvfn  34766  mrsubcv  35738  mrsubff  35740  mrsubrn  35741  mrsubccat  35746  unblimceq0lem  36812  ptrecube  37987  poimirlem24  38011  itg2addnclem2  38039  itg2gt0cn  38042  ibladdnclem  38043  itgaddnclem1  38045  iblabsnclem  38050  iblabsnc  38051  iblmulc2nc  38052  itgmulc2nclem1  38053  itggt0cn  38057  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  areacirc  38080  cdleme27cl  40858  dffltz  43084  cantnfub  43766  climsuse  46053  lptioo1  46077  icccncfext  46330  cncfiooicclem1  46336  iblsplit  46409  dirkerval2  46537  dirkerre  46538  fourierdlem9  46559  fourierdlem17  46567  fourierdlem43  46593  etransclem3  46680  etransclem7  46684  etransclem10  46687  etransclem21  46698  lincext1  48945