Theorem ifclda 4495

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ifcif 4460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461

This theorem is referenced by:  unxpdomlem3  9038  updjudhf  9698  acndom  9816  iunfictbso  9879  dfac12lem2  9909  ttukeylem6  10279  canthp1lem2  10418  xaddf  12967  xmulf  13015  ccatcl  14286  swrdcl  14367  ccatco  14557  lo1bdd2  15242  o1lo1  15255  sadadd2lem2  16166  sadcaddlem  16173  sadadd2lem  16175  sadadd3  16177  lcmfval  16335  iserodd  16545  prmreclem2  16627  prmreclem4  16629  prmreclem6  16631  prmrec  16632  vdwlem6  16696  mreexexd  17366  smndex2hbas  18564  symgextf  19034  pmtrf  19072  odfval  19149  cyggex2  19507  dprdfid  19629  dmdprdsplitlem  19649  sdrgacs  20078  cygznlem1  20783  cygznlem2a  20784  cygznlem3  20786  cygth  20788  fvmptnn04if  22007  chfacfisf  22012  chfacfisfcpmat  22013  ptpjpre2  22740  ptopn2  22744  ptpjopn  22772  iccpnfcnv  24116  xrhmeo  24118  cmetcaulem  24461  ovolunlem1a  24669  ovolunlem1  24670  ioorf  24746  mbfi1fseqlem3  24891  mbfi1flim  24897  itg2seq  24916  itg2splitlem  24922  itg2split  24923  iblss  24978  itgle  24983  itgeqa  24987  ibladdlem  24993  itgaddlem1  24996  iblabslem  25001  iblabs  25002  iblabsr  25003  iblmulc2  25004  itgmulc2lem1  25005  bddmulibl  25012  bddiblnc  25015  itggt0  25017  itgcn  25018  ellimc2  25050  limccnp  25064  limccnp2  25065  dvcobr  25119  lhop1  25187  elplyd  25372  coeeq2  25412  dvply1  25453  aalioulem3  25503  dvtaylp  25538  dvradcnv  25589  psercnlem1  25593  logcnlem2  25807  logcnlem3  25808  logcnlem4  25809  logtayllem  25823  logtayl  25824  cxpcl  25838  recxpcl  25839  leibpilem2  26100  leibpi  26101  rlimcnp2  26125  efrlim  26128  igamf  26209  igamcl  26210  pclogsum  26372  dchrelbasd  26396  lgsfcl2  26460  lgscllem  26461  lgsval2lem  26464  lgsne0  26492  2sqnn0  26595  dchrvmasumiflem2  26659  dchrisum0flblem1  26665  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntlemj  26760  padicabv  26787  crctcshwlkn0  28195  sgnsval  31437  xrge0iifcnv  31892  xrge0iifhom  31896  pnfneige0  31910  esumpinfval  32050  sigaclfu2  32098  ballotlemsv  32485  ballotlemsdom  32487  signswmnd  32545  signsvvf  32567  signsvfn  32570  mrsubcv  33481  mrsubff  33483  mrsubrn  33484  mrsubccat  33489  unblimceq0lem  34695  ptrecube  35786  poimirlem24  35810  itg2addnclem2  35838  itg2gt0cn  35841  ibladdnclem  35842  itgaddnclem1  35844  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  itgmulc2nclem1  35852  itggt0cn  35856  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  areacirc  35879  cdleme27cl  38387  selvval2lem5  40236  dffltz  40478  climsuse  43156  lptioo1  43180  icccncfext  43435  cncfiooicclem1  43441  iblsplit  43514  dirkerval2  43642  dirkerre  43643  fourierdlem9  43664  fourierdlem17  43672  fourierdlem43  43698  etransclem3  43785  etransclem7  43789  etransclem10  43792  etransclem21  43803  lincext1  45806