Theorem ifclda 4524

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  unxpdomlem3  9199  updjudhf  9884  acndom  10004  iunfictbso  10067  dfac12lem2  10098  ttukeylem6  10467  canthp1lem2  10606  xaddf  13184  xmulf  13232  ccatcl  14539  swrdcl  14610  ccatco  14801  lo1bdd2  15490  o1lo1  15503  sadadd2lem2  16420  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  lcmfval  16591  iserodd  16806  prmreclem2  16888  prmreclem4  16890  prmreclem6  16892  prmrec  16893  vdwlem6  16957  mreexexd  17609  smndex2hbas  18843  symgextf  19347  pmtrf  19385  odfval  19462  cyggex2  19827  dprdfid  19949  dmdprdsplitlem  19969  sdrgacs  20710  cygznlem1  21476  cygznlem2a  21477  cygznlem3  21479  cygth  21481  fvmptnn04if  22736  chfacfisf  22741  chfacfisfcpmat  22742  ptpjpre2  23467  ptopn2  23471  ptpjopn  23499  iccpnfcnv  24842  xrhmeo  24844  cmetcaulem  25188  ovolunlem1a  25397  ovolunlem1  25398  ioorf  25474  mbfi1fseqlem3  25618  mbfi1flim  25624  itg2seq  25643  itg2splitlem  25649  itg2split  25650  iblss  25706  itgle  25711  itgeqa  25715  ibladdlem  25721  itgaddlem1  25724  iblabslem  25729  iblabs  25730  iblabsr  25731  iblmulc2  25732  itgmulc2lem1  25733  bddmulibl  25740  bddiblnc  25743  itggt0  25745  itgcn  25746  ellimc2  25778  limccnp  25792  limccnp2  25793  dvcobr  25849  dvcobrOLD  25850  lhop1  25919  elplyd  26107  coeeq2  26147  dvply1  26191  aalioulem3  26242  dvtaylp  26278  dvradcnv  26330  psercnlem1  26335  logcnlem2  26552  logcnlem3  26553  logcnlem4  26554  logtayllem  26568  logtayl  26569  cxpcl  26583  recxpcl  26584  leibpilem2  26851  leibpi  26852  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  igamf  26961  igamcl  26962  pclogsum  27126  dchrelbasd  27150  lgsfcl2  27214  lgscllem  27215  lgsval2lem  27218  lgsne0  27246  2sqnn0  27349  dchrvmasumiflem2  27413  dchrisum0flblem1  27419  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntlemj  27514  padicabv  27541  crctcshwlkn0  29751  ccatws1f1o  32873  sgnsval  33118  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  gsummoncoe1fzo  33563  fldextrspunlsp  33669  xrge0iifcnv  33923  xrge0iifhom  33927  pnfneige0  33941  esumpinfval  34063  sigaclfu2  34111  ballotlemsv  34501  ballotlemsdom  34503  signswmnd  34548  signsvvf  34570  signsvfn  34573  mrsubcv  35497  mrsubff  35499  mrsubrn  35500  mrsubccat  35505  unblimceq0lem  36494  ptrecube  37614  poimirlem24  37638  itg2addnclem2  37666  itg2gt0cn  37669  ibladdnclem  37670  itgaddnclem1  37672  iblabsnclem  37677  iblabsnc  37678  iblmulc2nc  37679  itgmulc2nclem1  37680  itggt0cn  37684  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirc  37707  cdleme27cl  40360  selvcllem5  42570  selvvvval  42573  dffltz  42622  cantnfub  43310  climsuse  45606  lptioo1  45630  icccncfext  45885  cncfiooicclem1  45891  iblsplit  45964  dirkerval2  46092  dirkerre  46093  fourierdlem9  46114  fourierdlem17  46122  fourierdlem43  46148  etransclem3  46235  etransclem7  46239  etransclem10  46242  etransclem21  46253  lincext1  48443