Theorem ifclda 4506

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 4476	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 481	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2831	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4479	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 481	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2831	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 812	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4471

This theorem is referenced by:  unxpdomlem3  9137  updjudhf  9819  acndom  9937  iunfictbso  10000  dfac12lem2  10031  ttukeylem6  10400  canthp1lem2  10539  xaddf  13118  xmulf  13166  ccatcl  14476  swrdcl  14548  ccatco  14737  lo1bdd2  15426  o1lo1  15439  sadadd2lem2  16356  sadcaddlem  16363  sadadd2lem  16365  sadadd3  16367  lcmfval  16527  iserodd  16742  prmreclem2  16824  prmreclem4  16826  prmreclem6  16828  prmrec  16829  vdwlem6  16893  mreexexd  17549  smndex2hbas  18819  symgextf  19324  pmtrf  19362  odfval  19439  cyggex2  19804  dprdfid  19926  dmdprdsplitlem  19946  sdrgacs  20711  cygznlem1  21498  cygznlem2a  21499  cygznlem3  21501  cygth  21503  fvmptnn04if  22759  chfacfisf  22764  chfacfisfcpmat  22765  ptpjpre2  23490  ptopn2  23494  ptpjopn  23522  iccpnfcnv  24864  xrhmeo  24866  cmetcaulem  25210  ovolunlem1a  25419  ovolunlem1  25420  ioorf  25496  mbfi1fseqlem3  25640  mbfi1flim  25646  itg2seq  25665  itg2splitlem  25671  itg2split  25672  iblss  25728  itgle  25733  itgeqa  25737  ibladdlem  25743  itgaddlem1  25746  iblabslem  25751  iblabs  25752  iblabsr  25753  iblmulc2  25754  itgmulc2lem1  25755  bddmulibl  25762  bddiblnc  25765  itggt0  25767  itgcn  25768  ellimc2  25800  limccnp  25814  limccnp2  25815  dvcobr  25871  dvcobrOLD  25872  lhop1  25941  elplyd  26129  coeeq2  26169  dvply1  26213  aalioulem3  26264  dvtaylp  26300  dvradcnv  26352  psercnlem1  26357  logcnlem2  26574  logcnlem3  26575  logcnlem4  26576  logtayllem  26590  logtayl  26591  cxpcl  26605  recxpcl  26606  leibpilem2  26873  leibpi  26874  rlimcnp2  26898  efrlim  26901  efrlimOLD  26902  igamf  26983  igamcl  26984  pclogsum  27148  dchrelbasd  27172  lgsfcl2  27236  lgscllem  27237  lgsval2lem  27240  lgsne0  27268  2sqnn0  27371  dchrvmasumiflem2  27435  dchrisum0flblem1  27441  pntrlog2bndlem4  27513  pntrlog2bndlem5  27514  pntlemj  27536  padicabv  27563  crctcshwlkn0  29794  ccatws1f1o  32924  sgnsval  33122  elrgspnlem2  33202  elrgspnlem3  33203  elrgspnlem4  33204  gsummoncoe1fzo  33550  fldextrspunlsp  33679  extdgfialglem2  33698  xrge0iifcnv  33938  xrge0iifhom  33942  pnfneige0  33956  esumpinfval  34078  sigaclfu2  34126  ballotlemsv  34515  ballotlemsdom  34517  signswmnd  34562  signsvvf  34584  signsvfn  34587  mrsubcv  35546  mrsubff  35548  mrsubrn  35549  mrsubccat  35554  unblimceq0lem  36540  ptrecube  37660  poimirlem24  37684  itg2addnclem2  37712  itg2gt0cn  37715  ibladdnclem  37716  itgaddnclem1  37718  iblabsnclem  37723  iblabsnc  37724  iblmulc2nc  37725  itgmulc2nclem1  37726  itggt0cn  37730  ftc1anclem5  37737  ftc1anclem6  37738  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  areacirc  37753  cdleme27cl  40405  selvcllem5  42615  selvvvval  42618  dffltz  42667  cantnfub  43354  climsuse  45648  lptioo1  45672  icccncfext  45925  cncfiooicclem1  45931  iblsplit  46004  dirkerval2  46132  dirkerre  46133  fourierdlem9  46154  fourierdlem17  46162  fourierdlem43  46188  etransclem3  46275  etransclem7  46279  etransclem10  46282  etransclem21  46293  lincext1  48486