Theorem ifclda 4565

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531

This theorem is referenced by:  unxpdomlem3  9285  updjudhf  9968  acndom  10088  iunfictbso  10151  dfac12lem2  10182  ttukeylem6  10551  canthp1lem2  10690  xaddf  13262  xmulf  13310  ccatcl  14608  swrdcl  14679  ccatco  14870  lo1bdd2  15556  o1lo1  15569  sadadd2lem2  16483  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  lcmfval  16654  iserodd  16868  prmreclem2  16950  prmreclem4  16952  prmreclem6  16954  prmrec  16955  vdwlem6  17019  mreexexd  17692  smndex2hbas  18941  symgextf  19449  pmtrf  19487  odfval  19564  cyggex2  19929  dprdfid  20051  dmdprdsplitlem  20071  sdrgacs  20818  cygznlem1  21602  cygznlem2a  21603  cygznlem3  21605  cygth  21607  fvmptnn04if  22870  chfacfisf  22875  chfacfisfcpmat  22876  ptpjpre2  23603  ptopn2  23607  ptpjopn  23635  iccpnfcnv  24988  xrhmeo  24990  cmetcaulem  25335  ovolunlem1a  25544  ovolunlem1  25545  ioorf  25621  mbfi1fseqlem3  25766  mbfi1flim  25772  itg2seq  25791  itg2splitlem  25797  itg2split  25798  iblss  25854  itgle  25859  itgeqa  25863  ibladdlem  25869  itgaddlem1  25872  iblabslem  25877  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgmulc2lem1  25881  bddmulibl  25888  bddiblnc  25891  itggt0  25893  itgcn  25894  ellimc2  25926  limccnp  25940  limccnp2  25941  dvcobr  25997  dvcobrOLD  25998  lhop1  26067  elplyd  26255  coeeq2  26295  dvply1  26339  aalioulem3  26390  dvtaylp  26426  dvradcnv  26478  psercnlem1  26483  logcnlem2  26699  logcnlem3  26700  logcnlem4  26701  logtayllem  26715  logtayl  26716  cxpcl  26730  recxpcl  26731  leibpilem2  26998  leibpi  26999  rlimcnp2  27023  efrlim  27026  efrlimOLD  27027  igamf  27108  igamcl  27109  pclogsum  27273  dchrelbasd  27297  lgsfcl2  27361  lgscllem  27362  lgsval2lem  27365  lgsne0  27393  2sqnn0  27496  dchrvmasumiflem2  27560  dchrisum0flblem1  27566  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntlemj  27661  padicabv  27688  crctcshwlkn0  29850  ccatws1f1o  32920  sgnsval  33163  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  gsummoncoe1fzo  33597  xrge0iifcnv  33893  xrge0iifhom  33897  pnfneige0  33911  esumpinfval  34053  sigaclfu2  34101  ballotlemsv  34490  ballotlemsdom  34492  signswmnd  34550  signsvvf  34572  signsvfn  34575  mrsubcv  35494  mrsubff  35496  mrsubrn  35497  mrsubccat  35502  unblimceq0lem  36488  ptrecube  37606  poimirlem24  37630  itg2addnclem2  37658  itg2gt0cn  37661  ibladdnclem  37662  itgaddnclem1  37664  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  itgmulc2nclem1  37672  itggt0cn  37676  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  areacirc  37699  cdleme27cl  40348  selvcllem5  42568  selvvvval  42571  dffltz  42620  cantnfub  43310  climsuse  45563  lptioo1  45587  icccncfext  45842  cncfiooicclem1  45848  iblsplit  45921  dirkerval2  46049  dirkerre  46050  fourierdlem9  46071  fourierdlem17  46079  fourierdlem43  46105  etransclem3  46192  etransclem7  46196  etransclem10  46199  etransclem21  46210  lincext1  48299