Theorem ifcld 4511

Description: Membership (closure) of a conditional operator, deduction form. (Contributed by SO, 16-Jul-2018.)

Hypotheses

Ref	Expression
ifcld.a	⊢ (𝜑 → 𝐴 ∈ 𝐶)
ifcld.b	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
ifcld	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifcld

Step	Hyp	Ref	Expression
1		ifcld.a	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
2		ifcld.b	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
3		ifcl 4510	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
4	1, 2, 3	syl2anc 586	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2110  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4467

This theorem is referenced by:  soltmin  5995  pw2f1olem  8620  unxpdomlem3  8723  wemaplem2  9010  cantnfp1lem1  9140  cantnfp1lem2  9141  cantnfp1lem3  9142  cantnflem1d  9150  cantnflem1  9151  ssfzunsnext  12951  relexpsucnnr  14383  rexuzre  14711  rexico  14712  limsupgre  14837  rlim3  14854  o1lo1  14893  rlimclim1  14901  lo1resb  14920  o1resb  14922  o1of2  14968  o1rlimmul  14974  lo1le  15007  ruclem1  15583  ruclem10  15591  bitsfzo  15783  ramub1lem2  16362  ramcl  16364  prmocl  16369  prmop1  16373  prmdvdsprmo  16377  prmolefac  16381  prmodvdslcmf  16382  prmgapprmo  16397  setsstruct2  16520  wunress  16563  opifismgm  17868  mulgfval  18225  frgpuptf  18895  gsumzsplit  19046  gsummpt1n0  19084  snifpsrbag  20145  psr1cl  20181  subrgpsr  20198  mvrf  20203  mplmon  20243  mplmonmul  20244  mplcoe1  20245  evlslem3  20292  evlslem1  20294  coe1tmfv2  20442  gsummoncoe1  20471  xrsds  20587  uvcvvcl2  20931  uvcff  20934  mamumat1cl  21047  dmatmulcl  21108  scmatscmiddistr  21116  1mavmul  21156  marrepeval  21171  marrepcl  21172  marepveval  21176  marepvcl  21177  mdetrsca2  21212  mdetr0  21213  mdetrlin2  21215  mdetralt2  21217  mdetero  21218  mdetunilem2  21221  mdetunilem5  21224  mdetunilem6  21225  mdetunilem8  21227  mdetunilem9  21228  maducoeval2  21248  maduf  21249  madutpos  21250  madugsum  21251  gsummatr01lem3  21265  marep01ma  21268  smadiadetglem2  21280  monmatcollpw  21386  pmatcollpw3fi1lem1  21393  pmatcollpw3fi1lem2  21394  xkopt  22262  tsmssplit  22759  ssblex  23037  stdbdxmet  23124  stdbdmet  23125  stdbdbl  23126  stdbdmopn  23127  nlmvscnlem1  23294  tgioo  23403  xrsxmet  23416  icccmplem2  23430  ipcnlem1  23847  ivthlem2  24052  ovolicc2lem5  24121  ioombl1lem1  24158  ioombl1lem3  24160  ioombl1lem4  24161  mbfmax  24249  i1fres  24305  itg1climres  24314  mbfi1fseqlem3  24317  mbfi1fseqlem4  24318  mbfi1fseqlem5  24319  limcres  24483  dvferm1lem  24580  dvferm2lem  24582  dvlip2  24591  lhop1  24610  dvfsumrlim  24627  mdegaddle  24667  deg1addle2  24695  deg1sublt  24703  ply1divmo  24728  plyaddlem1  24802  plyaddlem  24804  coeaddlem  24838  dgradd2  24857  plydiveu  24886  abelthlem9  25027  logcnlem2  25225  logcnlem3  25226  cxpcn3lem  25327  lgamgulmlem4  25608  lgamgulmlem6  25610  ftalem2  25650  gausslemma2dlem4  25944  chebbnd1lem1  26044  dchrisumlem3  26066  dchrvmasumiflem1  26076  ostth3  26213  axlowdimlem15  26741  dstfrvunirn  31732  circlemeth  31911  indispconn  32481  ex-sategoelel  32668  ex-sategoelelomsuc  32673  noprefixmo  33202  knoppndvlem18  33868  itg2addnclem2  34943  itg2addnclem3  34944  ftc1anclem5  34970  dffltz  39269  irrapxlem4  39420  irrapxlem5  39421  kelac1  39661  areaquad  39821  clsk1indlem4  40392  refsum2cnlem1  41292  rexabslelem  41690  uzublem  41702  ioondisj2  41765  ioondisj1  41766  uzubioo  41841  mullimc  41895  mullimcf  41902  lptioo2  41910  limcleqr  41923  0ellimcdiv  41928  limsupubuzlem  41991  limsupequzmptlem  42007  climxrre  42029  limsup10exlem  42051  limsup10ex  42052  liminf10ex  42053  liminflelimsuplem  42054  icccncfext  42168  cncfiooicclem1  42174  ioodvbdlimc1lem2  42215  ioodvbdlimc2lem  42217  stoweid  42347  fourierdlem9  42400  fourierdlem10  42401  fourierdlem37  42428  fourierdlem40  42431  fourierdlem66  42456  fourierdlem73  42463  fourierdlem74  42464  fourierdlem75  42465  fourierdlem78  42468  fourierdlem79  42469  fourierdlem95  42485  fourierdlem103  42493  sqwvfoura  42512  fouriersw  42515  etransclem1  42519  etransclem4  42522  etransclem17  42535  etransclem18  42536  etransclem19  42537  etransclem20  42538  etransclem21  42539  etransclem22  42540  etransclem23  42541  etransclem27  42545  etransclem32  42550  etransclem35  42553  etransclem46  42564  ioorrnopnlem  42588  ovnval2  42826  volicorecl  42827  hoiprodcl  42828  ovnf  42844  hsphoif  42857  hsphoival  42860  hoiprodcl3  42861  volicore  42862  hoidmvcl  42863  hsphoidmvle2  42866  hsphoidmvle  42867  hoidmv1lelem1  42872  hoidmv1lelem2  42873  hoidmv1lelem3  42874  hoidmvlelem2  42877  hoidmvlelem3  42878  ovnhoilem1  42882  hoidifhspf  42899  hoidifhspval3  42900  ovolval4lem1  42930  ovolval4lem2  42931  smfmullem1  43065  smfmullem2  43066  smfmullem3  43067  afv2ex  43412  suppmptcfin  44426  linc1  44479  lcoss  44490  el0ldep  44520