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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4480

This theorem is referenced by:  unxpdomlem3  9196  updjudhf  9884  acndom  10002  iunfictbso  10065  dfac12lem2  10096  ttukeylem6  10466  canthp1lem2  10606  xaddf  13222  xmulf  13270  ccatcl  14582  swrdcl  14654  ccatco  14843  lo1bdd2  15532  o1lo1  15545  sadadd2lem2  16465  sadcaddlem  16472  sadadd2lem  16474  sadadd3  16476  lcmfval  16636  iserodd  16852  prmreclem2  16934  prmreclem4  16936  prmreclem6  16938  prmrec  16939  vdwlem6  17003  mreexexd  17661  smndex2hbas  18934  symgextf  19438  pmtrf  19476  odfval  19553  cyggex2  19918  dprdfid  20040  dmdprdsplitlem  20060  sdrgacs  20828  cygznlem1  21596  cygznlem2a  21597  cygznlem3  21599  cygth  21601  selvcllem5  22170  selvvvval  22173  fvmptnn04if  22887  chfacfisf  22892  chfacfisfcpmat  22893  ptpjpre2  23618  ptopn2  23622  ptpjopn  23650  iccpnfcnv  24984  xrhmeo  24986  cmetcaulem  25328  ovolunlem1a  25536  ovolunlem1  25537  ioorf  25613  mbfi1fseqlem3  25757  mbfi1flim  25763  itg2seq  25782  itg2splitlem  25788  itg2split  25789  iblss  25845  itgle  25850  itgeqa  25854  ibladdlem  25860  itgaddlem1  25863  iblabslem  25868  iblabs  25869  iblabsr  25870  iblmulc2  25871  itgmulc2lem1  25872  bddmulibl  25879  bddiblnc  25882  itggt0  25884  itgcn  25885  ellimc2  25917  limccnp  25931  limccnp2  25932  dvcobr  25986  lhop1  26054  elplyd  26240  coeeq2  26280  dvply1  26323  aalioulem3  26373  dvtaylp  26408  dvradcnv  26459  psercnlem1  26463  logcnlem2  26683  logcnlem3  26684  logcnlem4  26685  logtayllem  26699  logtayl  26700  cxpcl  26714  recxpcl  26715  leibpilem2  26981  leibpi  26982  rlimcnp2  27006  efrlim  27009  igamf  27090  igamcl  27091  pclogsum  27254  dchrelbasd  27278  lgsfcl2  27342  lgscllem  27343  lgsval2lem  27346  lgsne0  27374  2sqnn0  27477  dchrvmasumiflem2  27541  dchrisum0flblem1  27547  pntrlog2bndlem4  27619  pntrlog2bndlem5  27620  pntlemj  27642  padicabv  27669  crctcshwlkn0  29965  ccatws1f1o  33088  sgnsval  33300  elrgspnlem2  33383  elrgspnlem3  33384  elrgspnlem4  33385  gsummoncoe1fzo  33752  selvascl  33773  fldextrspunlsp  33930  extdgfialglem2  33949  xrge0iifcnv  34189  xrge0iifhom  34193  pnfneige0  34207  esumpinfval  34329  sigaclfu2  34377  ballotlemsv  34766  ballotlemsdom  34768  signswmnd  34813  signsvvf  34835  signsvfn  34838  mrsubcv  35813  mrsubff  35815  mrsubrn  35816  mrsubccat  35821  unblimceq0lem  36897  ptrecube  38072  poimirlem24  38096  itg2addnclem2  38124  itg2gt0cn  38127  ibladdnclem  38128  itgaddnclem1  38130  iblabsnclem  38135  iblabsnc  38136  iblmulc2nc  38137  itgmulc2nclem1  38138  itggt0cn  38142  ftc1anclem5  38149  ftc1anclem6  38150  ftc1anclem7  38151  ftc1anclem8  38152  ftc1anc  38153  areacirc  38165  cdleme27cl  40943  dffltz  43169  cantnfub  43851  climsuse  46137  lptioo1  46161  icccncfext  46414  cncfiooicclem1  46420  iblsplit  46493  dirkerval2  46621  dirkerre  46622  fourierdlem9  46643  fourierdlem17  46651  fourierdlem43  46677  etransclem3  46764  etransclem7  46768  etransclem10  46771  etransclem21  46782  lincext1  49029