Theorem ifclda 4583

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  unxpdomlem3  9315  updjudhf  10000  acndom  10120  iunfictbso  10183  dfac12lem2  10214  ttukeylem6  10583  canthp1lem2  10722  xaddf  13286  xmulf  13334  ccatcl  14622  swrdcl  14693  ccatco  14884  lo1bdd2  15570  o1lo1  15583  sadadd2lem2  16496  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  lcmfval  16668  iserodd  16882  prmreclem2  16964  prmreclem4  16966  prmreclem6  16968  prmrec  16969  vdwlem6  17033  mreexexd  17706  smndex2hbas  18951  symgextf  19459  pmtrf  19497  odfval  19574  cyggex2  19939  dprdfid  20061  dmdprdsplitlem  20081  sdrgacs  20824  cygznlem1  21608  cygznlem2a  21609  cygznlem3  21611  cygth  21613  fvmptnn04if  22876  chfacfisf  22881  chfacfisfcpmat  22882  ptpjpre2  23609  ptopn2  23613  ptpjopn  23641  iccpnfcnv  24994  xrhmeo  24996  cmetcaulem  25341  ovolunlem1a  25550  ovolunlem1  25551  ioorf  25627  mbfi1fseqlem3  25772  mbfi1flim  25778  itg2seq  25797  itg2splitlem  25803  itg2split  25804  iblss  25860  itgle  25865  itgeqa  25869  ibladdlem  25875  itgaddlem1  25878  iblabslem  25883  iblabs  25884  iblabsr  25885  iblmulc2  25886  itgmulc2lem1  25887  bddmulibl  25894  bddiblnc  25897  itggt0  25899  itgcn  25900  ellimc2  25932  limccnp  25946  limccnp2  25947  dvcobr  26003  dvcobrOLD  26004  lhop1  26073  elplyd  26261  coeeq2  26301  dvply1  26343  aalioulem3  26394  dvtaylp  26430  dvradcnv  26482  psercnlem1  26487  logcnlem2  26703  logcnlem3  26704  logcnlem4  26705  logtayllem  26719  logtayl  26720  cxpcl  26734  recxpcl  26735  leibpilem2  27002  leibpi  27003  rlimcnp2  27027  efrlim  27030  efrlimOLD  27031  igamf  27112  igamcl  27113  pclogsum  27277  dchrelbasd  27301  lgsfcl2  27365  lgscllem  27366  lgsval2lem  27369  lgsne0  27397  2sqnn0  27500  dchrvmasumiflem2  27564  dchrisum0flblem1  27570  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntlemj  27665  padicabv  27692  crctcshwlkn0  29854  ccatws1f1o  32918  sgnsval  33154  gsummoncoe1fzo  33583  xrge0iifcnv  33879  xrge0iifhom  33883  pnfneige0  33897  esumpinfval  34037  sigaclfu2  34085  ballotlemsv  34474  ballotlemsdom  34476  signswmnd  34534  signsvvf  34556  signsvfn  34559  mrsubcv  35478  mrsubff  35480  mrsubrn  35481  mrsubccat  35486  unblimceq0lem  36472  ptrecube  37580  poimirlem24  37604  itg2addnclem2  37632  itg2gt0cn  37635  ibladdnclem  37636  itgaddnclem1  37638  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  itgmulc2nclem1  37646  itggt0cn  37650  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  areacirc  37673  cdleme27cl  40323  selvcllem5  42537  selvvvval  42540  dffltz  42589  cantnfub  43283  climsuse  45529  lptioo1  45553  icccncfext  45808  cncfiooicclem1  45814  iblsplit  45887  dirkerval2  46015  dirkerre  46016  fourierdlem9  46037  fourierdlem17  46045  fourierdlem43  46071  etransclem3  46158  etransclem7  46162  etransclem10  46165  etransclem21  46176  lincext1  48183