Theorem ifclda 4515

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

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

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  unxpdomlem3  9158  updjudhf  9843  acndom  9961  iunfictbso  10024  dfac12lem2  10055  ttukeylem6  10424  canthp1lem2  10564  xaddf  13139  xmulf  13187  ccatcl  14497  swrdcl  14569  ccatco  14758  lo1bdd2  15447  o1lo1  15460  sadadd2lem2  16377  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  lcmfval  16548  iserodd  16763  prmreclem2  16845  prmreclem4  16847  prmreclem6  16849  prmrec  16850  vdwlem6  16914  mreexexd  17571  smndex2hbas  18841  symgextf  19346  pmtrf  19384  odfval  19461  cyggex2  19826  dprdfid  19948  dmdprdsplitlem  19968  sdrgacs  20734  cygznlem1  21521  cygznlem2a  21522  cygznlem3  21524  cygth  21526  fvmptnn04if  22793  chfacfisf  22798  chfacfisfcpmat  22799  ptpjpre2  23524  ptopn2  23528  ptpjopn  23556  iccpnfcnv  24898  xrhmeo  24900  cmetcaulem  25244  ovolunlem1a  25453  ovolunlem1  25454  ioorf  25530  mbfi1fseqlem3  25674  mbfi1flim  25680  itg2seq  25699  itg2splitlem  25705  itg2split  25706  iblss  25762  itgle  25767  itgeqa  25771  ibladdlem  25777  itgaddlem1  25780  iblabslem  25785  iblabs  25786  iblabsr  25787  iblmulc2  25788  itgmulc2lem1  25789  bddmulibl  25796  bddiblnc  25799  itggt0  25801  itgcn  25802  ellimc2  25834  limccnp  25848  limccnp2  25849  dvcobr  25905  dvcobrOLD  25906  lhop1  25975  elplyd  26163  coeeq2  26203  dvply1  26247  aalioulem3  26298  dvtaylp  26334  dvradcnv  26386  psercnlem1  26391  logcnlem2  26608  logcnlem3  26609  logcnlem4  26610  logtayllem  26624  logtayl  26625  cxpcl  26639  recxpcl  26640  leibpilem2  26907  leibpi  26908  rlimcnp2  26932  efrlim  26935  efrlimOLD  26936  igamf  27017  igamcl  27018  pclogsum  27182  dchrelbasd  27206  lgsfcl2  27270  lgscllem  27271  lgsval2lem  27274  lgsne0  27302  2sqnn0  27405  dchrvmasumiflem2  27469  dchrisum0flblem1  27475  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntlemj  27570  padicabv  27597  crctcshwlkn0  29894  ccatws1f1o  33033  sgnsval  33243  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  gsummoncoe1fzo  33678  fldextrspunlsp  33831  extdgfialglem2  33850  xrge0iifcnv  34090  xrge0iifhom  34094  pnfneige0  34108  esumpinfval  34230  sigaclfu2  34278  ballotlemsv  34667  ballotlemsdom  34669  signswmnd  34714  signsvvf  34736  signsvfn  34739  mrsubcv  35704  mrsubff  35706  mrsubrn  35707  mrsubccat  35712  unblimceq0lem  36706  ptrecube  37821  poimirlem24  37845  itg2addnclem2  37873  itg2gt0cn  37876  ibladdnclem  37877  itgaddnclem1  37879  iblabsnclem  37884  iblabsnc  37885  iblmulc2nc  37886  itgmulc2nclem1  37887  itggt0cn  37891  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  areacirc  37914  cdleme27cl  40626  selvcllem5  42825  selvvvval  42828  dffltz  42877  cantnfub  43563  climsuse  45854  lptioo1  45878  icccncfext  46131  cncfiooicclem1  46137  iblsplit  46210  dirkerval2  46338  dirkerre  46339  fourierdlem9  46360  fourierdlem17  46368  fourierdlem43  46394  etransclem3  46481  etransclem7  46485  etransclem10  46488  etransclem21  46499  lincext1  48700