Theorem ifclda 4517

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 4487	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifclda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5		iffalse 4490	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifclda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 ∈ 𝐶)
8	6, 7	eqeltrd 2860	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
9	4, 8	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  unxpdomlem3  9253  updjudhf  10016  acndom  10134  iunfictbso  10197  dfac12lem2  10227  ttukeylem6  10596  canthp1lem2  10742  xaddf  13358  xmulf  13406  ccatcl  14723  swrdcl  14798  ccatco  14991  lo1bdd2  15697  o1lo1  15710  sadadd2lem2  16626  sadcaddlem  16633  sadadd2lem  16635  sadadd3  16637  lcmfval  16802  iserodd  17019  prmreclem2  17101  prmreclem4  17103  prmreclem6  17105  prmrec  17106  vdwlem6  17170  mreexexd  17828  smndex2hbas  19121  symgextf  19637  pmtrf  19675  odfval  19752  cyggex2  20117  dprdfid  20239  dmdprdsplitlem  20259  sdrgacs  21064  cygznlem1  21878  cygznlem2a  21879  cygznlem3  21881  cygth  21883  selvcllem5  22454  selvvvval  22457  fvmptnn04if  23173  chfacfisf  23178  chfacfisfcpmat  23179  ptpjpre2  23905  ptopn2  23909  ptpjopn  23937  iccpnfcnv  25271  xrhmeo  25273  cmetcaulem  25615  ovolunlem1a  25823  ovolunlem1  25824  ioorf  25900  mbfi1fseqlem3  26044  mbfi1flim  26050  itg2seq  26069  itg2splitlem  26075  itg2split  26076  iblss  26131  itgle  26136  itgeqa  26140  ibladdlem  26146  itgaddlem1  26149  iblabslem  26154  iblabs  26155  iblabsr  26156  iblmulc2  26157  itgmulc2lem1  26158  bddmulibl  26165  bddiblnc  26168  itggt0  26170  itgcn  26171  ellimc2  26203  limccnp  26217  limccnp2  26218  dvcobr  26272  lhop1  26340  elplyd  26526  coeeq2  26567  dvply1  26611  aalioulem3  26667  dvtaylp  26703  dvradcnv  26754  psercnlem1  26758  logcnlem2  26977  logcnlem3  26978  logcnlem4  26979  logtayllem  26993  logtayl  26994  cxpcl  27008  recxpcl  27009  leibpilem2  27275  leibpi  27276  rlimcnp2  27300  efrlim  27303  igamf  27384  igamcl  27385  pclogsum  27548  dchrelbasd  27572  lgsfcl2  27636  lgscllem  27637  lgsval2lem  27640  lgsne0  27668  2sqnn0  27771  dchrvmasumiflem2  27835  dchrisum0flblem1  27841  pntrlog2bndlem4  27913  pntrlog2bndlem5  27914  pntlemj  27936  padicabv  27963  crctcshwlkn0  30416  ccatws1f1o  33561  sgnsval  33769  elrgspnlem2  33851  elrgspnlem3  33852  elrgspnlem4  33853  gsummoncoe1fzo  34176  selvascl  34196  fldextrspunlsp  34353  extdgfialglem2  34372  xrge0iifcnv  34612  xrge0iifhom  34616  pnfneige0  34630  esumpinfval  34752  sigaclfu2  34800  ballotlemsv  35189  ballotlemsdom  35191  signswmnd  35233  signsvvf  35255  signsvfn  35258  mrsubcv  36362  mrsubff  36364  mrsubrn  36365  mrsubccat  36370  unblimceq0lem  37465  ptrecube  38632  poimirlem24  38656  itg2addnclem2  38684  itg2gt0cn  38687  ibladdnclem  38688  itgaddnclem1  38690  iblabsnclem  38695  iblabsnc  38696  iblmulc2nc  38697  itgmulc2nclem1  38698  itggt0cn  38702  ftc1anclem5  38709  ftc1anclem6  38710  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  areacirc  38725  cdleme27cl  41517  dffltz  43764  cantnfub  44417  climsuse  46714  lptioo1  46738  icccncfext  46991  cncfiooicclem1  46997  iblsplit  47070  dirkerval2  47198  dirkerre  47199  fourierdlem9  47220  fourierdlem17  47228  fourierdlem43  47254  etransclem3  47341  etransclem7  47345  etransclem10  47348  etransclem21  47359  lincext1  49660