Theorem ifclda 4070

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  unxpdomlem3  8051  acndom  8757  iunfictbso  8820  dfac12lem2  8849  ttukeylem6  9219  canthp1lem2  9354  xaddf  11929  xmulf  11974  ccatcl  13212  swrdcl  13271  ccatco  13432  lo1bdd2  14103  o1lo1  14116  sadadd2lem2  15010  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  lcmfval  15172  iserodd  15378  prmreclem2  15459  prmreclem4  15461  prmreclem6  15463  prmrec  15464  vdwlem6  15528  mreexexd  16131  symgextf  17660  pmtrf  17698  cyggex2  18121  dprdfid  18239  dmdprdsplitlem  18259  cygznlem1  19734  cygznlem2a  19735  cygznlem3  19737  cygth  19739  fvmptnn04if  20473  chfacfisf  20478  chfacfisfcpmat  20479  ptpjpre2  21193  ptopn2  21197  ptpjopn  21225  iccpnfcnv  22551  xrhmeo  22553  cmetcaulem  22894  ovolunlem1a  23071  ovolunlem1  23072  ioorf  23147  mbfi1fseqlem3  23290  mbfi1flim  23296  itg2seq  23315  itg2splitlem  23321  itg2split  23322  iblss  23377  itgle  23382  itgeqa  23386  ibladdlem  23392  itgaddlem1  23395  iblabslem  23400  iblabs  23401  iblabsr  23402  iblmulc2  23403  itgmulc2lem1  23404  bddmulibl  23411  itggt0  23414  itgcn  23415  ellimc2  23447  limccnp  23461  limccnp2  23462  dvcobr  23515  lhop1  23581  elplyd  23762  coeeq2  23802  dvply1  23843  aalioulem3  23893  dvtaylp  23928  dvradcnv  23979  psercnlem1  23983  logcnlem2  24189  logcnlem3  24190  logcnlem4  24191  logtayllem  24205  logtayl  24206  cxpcl  24220  recxpcl  24221  leibpilem2  24468  leibpi  24469  rlimcnp2  24493  efrlim  24496  igamf  24577  igamcl  24578  pclogsum  24740  dchrelbasd  24764  lgsfcl2  24828  lgscllem  24829  lgsval2lem  24832  lgsne0  24860  dchrvmasumiflem2  24991  dchrisum0flblem1  24997  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntlemj  25092  padicabv  25119  sgnsval  29059  xrge0iifcnv  29307  xrge0iifhom  29311  pnfneige0  29325  esumpinfval  29462  sigaclfu2  29511  ballotlemsv  29898  ballotlemsdom  29900  signswmnd  29960  signsvvf  29982  signsvfn  29985  mrsubcv  30661  mrsubff  30663  mrsubrn  30664  mrsubccat  30669  unblimceq0lem  31667  ptrecube  32579  poimirlem24  32603  itg2addnclem2  32632  itg2gt0cn  32635  ibladdnclem  32636  itgaddnclem1  32638  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  itgmulc2nclem1  32646  bddiblnc  32650  itggt0cn  32652  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  areacirc  32675  cdleme27cl  34672  sdrgacs  36790  climsuse  38675  lptioo1  38699  icccncfext  38773  cncfiooicclem1  38779  iblsplit  38858  dirkerval2  38987  dirkerre  38988  fourierdlem9  39009  fourierdlem17  39017  fourierdlem43  39043  etransclem3  39130  etransclem7  39134  etransclem10  39137  etransclem21  39148  crctcsh1wlkn0  41024  lincext1  42037