Theorem ifclda 4541

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-if 4506

This theorem is referenced by:  unxpdomlem3  9265  updjudhf  9950  acndom  10070  iunfictbso  10133  dfac12lem2  10164  ttukeylem6  10533  canthp1lem2  10672  xaddf  13245  xmulf  13293  ccatcl  14597  swrdcl  14668  ccatco  14859  lo1bdd2  15545  o1lo1  15558  sadadd2lem2  16474  sadcaddlem  16481  sadadd2lem  16483  sadadd3  16485  lcmfval  16645  iserodd  16860  prmreclem2  16942  prmreclem4  16944  prmreclem6  16946  prmrec  16947  vdwlem6  17011  mreexexd  17665  smndex2hbas  18899  symgextf  19403  pmtrf  19441  odfval  19518  cyggex2  19883  dprdfid  20005  dmdprdsplitlem  20025  sdrgacs  20766  cygznlem1  21532  cygznlem2a  21533  cygznlem3  21535  cygth  21537  fvmptnn04if  22792  chfacfisf  22797  chfacfisfcpmat  22798  ptpjpre2  23523  ptopn2  23527  ptpjopn  23555  iccpnfcnv  24898  xrhmeo  24900  cmetcaulem  25245  ovolunlem1a  25454  ovolunlem1  25455  ioorf  25531  mbfi1fseqlem3  25675  mbfi1flim  25681  itg2seq  25700  itg2splitlem  25706  itg2split  25707  iblss  25763  itgle  25768  itgeqa  25772  ibladdlem  25778  itgaddlem1  25781  iblabslem  25786  iblabs  25787  iblabsr  25788  iblmulc2  25789  itgmulc2lem1  25790  bddmulibl  25797  bddiblnc  25800  itggt0  25802  itgcn  25803  ellimc2  25835  limccnp  25849  limccnp2  25850  dvcobr  25906  dvcobrOLD  25907  lhop1  25976  elplyd  26164  coeeq2  26204  dvply1  26248  aalioulem3  26299  dvtaylp  26335  dvradcnv  26387  psercnlem1  26392  logcnlem2  26609  logcnlem3  26610  logcnlem4  26611  logtayllem  26625  logtayl  26626  cxpcl  26640  recxpcl  26641  leibpilem2  26908  leibpi  26909  rlimcnp2  26933  efrlim  26936  efrlimOLD  26937  igamf  27018  igamcl  27019  pclogsum  27183  dchrelbasd  27207  lgsfcl2  27271  lgscllem  27272  lgsval2lem  27275  lgsne0  27303  2sqnn0  27406  dchrvmasumiflem2  27470  dchrisum0flblem1  27476  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  pntlemj  27571  padicabv  27598  crctcshwlkn0  29808  ccatws1f1o  32932  sgnsval  33177  elrgspnlem2  33243  elrgspnlem3  33244  elrgspnlem4  33245  gsummoncoe1fzo  33612  fldextrspunlsp  33720  xrge0iifcnv  33969  xrge0iifhom  33973  pnfneige0  33987  esumpinfval  34109  sigaclfu2  34157  ballotlemsv  34547  ballotlemsdom  34549  signswmnd  34594  signsvvf  34616  signsvfn  34619  mrsubcv  35537  mrsubff  35539  mrsubrn  35540  mrsubccat  35545  unblimceq0lem  36529  ptrecube  37649  poimirlem24  37673  itg2addnclem2  37701  itg2gt0cn  37704  ibladdnclem  37705  itgaddnclem1  37707  iblabsnclem  37712  iblabsnc  37713  iblmulc2nc  37714  itgmulc2nclem1  37715  itggt0cn  37719  ftc1anclem5  37726  ftc1anclem6  37727  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730  areacirc  37742  cdleme27cl  40390  selvcllem5  42580  selvvvval  42583  dffltz  42632  cantnfub  43320  climsuse  45617  lptioo1  45641  icccncfext  45896  cncfiooicclem1  45902  iblsplit  45975  dirkerval2  46103  dirkerre  46104  fourierdlem9  46125  fourierdlem17  46133  fourierdlem43  46159  etransclem3  46246  etransclem7  46250  etransclem10  46253  etransclem21  46264  lincext1  48410