Theorem ifcld 4131

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 4130	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
4	1, 2, 3	syl2anc 693	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 1990  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  soltmin  5532  pw2f1olem  8064  unxpdomlem3  8166  wemaplem2  8452  cantnfp1lem1  8575  cantnfp1lem2  8576  cantnfp1lem3  8577  cantnflem1d  8585  cantnflem1  8586  ssfzunsnext  12386  relexpsucnnr  13765  rexuzre  14092  rexico  14093  limsupgre  14212  rlim3  14229  o1lo1  14268  rlimclim1  14276  lo1resb  14295  o1resb  14297  o1of2  14343  o1rlimmul  14349  lo1le  14382  ruclem1  14960  ruclem10  14968  bitsfzo  15157  ramub1lem2  15731  ramcl  15733  prmocl  15738  prmop1  15742  prmdvdsprmo  15746  prmolefac  15750  prmodvdslcmf  15751  prmgapprmo  15766  setsstruct2  15896  setsstructOLD  15899  wunress  15940  opifismgm  17258  frgpuptf  18183  gsumzsplit  18327  gsummpt1n0  18364  snifpsrbag  19366  psr1cl  19402  subrgpsr  19419  mvrf  19424  mplmon  19463  mplmonmul  19464  mplcoe1  19465  evlslem3  19514  evlslem1  19515  coe1tmfv2  19645  gsummoncoe1  19674  xrsds  19789  uvcvvcl2  20127  uvcff  20130  mamumat1cl  20245  dmatmulcl  20306  scmatscmiddistr  20314  1mavmul  20354  marrepeval  20369  marrepcl  20370  marepveval  20374  marepvcl  20375  mdetrsca2  20410  mdetr0  20411  mdetrlin2  20413  mdetralt2  20415  mdetero  20416  mdetunilem2  20419  mdetunilem5  20422  mdetunilem6  20423  mdetunilem8  20425  mdetunilem9  20426  maducoeval2  20446  maduf  20447  madutpos  20448  madugsum  20449  gsummatr01lem3  20463  marep01ma  20466  smadiadetglem2  20478  monmatcollpw  20584  pmatcollpw3fi1lem1  20591  pmatcollpw3fi1lem2  20592  xkopt  21458  tsmssplit  21955  ssblex  22233  stdbdxmet  22320  stdbdmet  22321  stdbdbl  22322  stdbdmopn  22323  nlmvscnlem1  22490  tgioo  22599  xrsxmet  22612  icccmplem2  22626  ipcnlem1  23044  ivthlem2  23221  ovolicc2lem5  23289  ioombl1lem1  23326  ioombl1lem3  23328  ioombl1lem4  23329  mbfmax  23416  i1fres  23472  itg1climres  23481  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  limcres  23650  dvferm1lem  23747  dvferm2lem  23749  dvlip2  23758  lhop1  23777  dvfsumrlim  23794  mdegaddle  23834  deg1addle2  23862  deg1sublt  23870  ply1divmo  23895  plyaddlem1  23969  plyaddlem  23971  coeaddlem  24005  dgradd2  24024  plydiveu  24053  abelthlem9  24194  logcnlem2  24389  logcnlem3  24390  cxpcn3lem  24488  lgamgulmlem4  24758  lgamgulmlem6  24760  ftalem2  24800  gausslemma2dlem4  25094  chebbnd1lem1  25158  dchrisumlem3  25180  dchrvmasumiflem1  25190  ostth3  25327  axlowdimlem15  25836  dstfrvunirn  30536  circlemeth  30718  indispconn  31216  noprefixmo  31848  knoppndvlem18  32520  itg2addnclem2  33462  itg2addnclem3  33463  ftc1anclem5  33489  irrapxlem4  37389  irrapxlem5  37390  kelac1  37633  areaquad  37802  clsk1indlem4  38342  refsum2cnlem1  39196  rexabslelem  39645  uzublem  39657  ioondisj2  39714  ioondisj1  39715  uzubioo  39794  mullimc  39848  mullimcf  39855  lptioo2  39863  limcleqr  39876  0ellimcdiv  39881  limsupubuzlem  39944  limsupequzmptlem  39960  climxrre  39982  limsup10exlem  40004  limsup10ex  40005  liminf10ex  40006  liminflelimsuplem  40007  icccncfext  40100  cncfiooicclem1  40106  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweid  40280  fourierdlem9  40333  fourierdlem10  40334  fourierdlem37  40361  fourierdlem40  40364  fourierdlem66  40389  fourierdlem73  40396  fourierdlem74  40397  fourierdlem75  40398  fourierdlem78  40401  fourierdlem79  40402  fourierdlem95  40418  fourierdlem103  40426  sqwvfoura  40445  fouriersw  40448  etransclem1  40452  etransclem4  40455  etransclem17  40468  etransclem18  40469  etransclem19  40470  etransclem20  40471  etransclem21  40472  etransclem22  40473  etransclem23  40474  etransclem27  40478  etransclem32  40483  etransclem35  40486  etransclem46  40497  ioorrnopnlem  40524  ovnval2  40759  volicorecl  40760  hoiprodcl  40761  ovnf  40777  hsphoif  40790  hsphoival  40793  hoiprodcl3  40794  volicore  40795  hoidmvcl  40796  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmvlelem2  40810  hoidmvlelem3  40811  ovnhoilem1  40815  hoidifhspf  40832  hoidifhspval3  40833  ovolval4lem1  40863  ovolval4lem2  40864  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  suppmptcfin  42160  linc1  42214  lcoss  42225  el0ldep  42255