Theorem ifcld 4567

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

Syntax hints:   → wi 4   ∈ wcel 2098  ifcif 4521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-if 4522

This theorem is referenced by:  ifexd  4569  soltmin  6128  pw2f1olem  9073  unxpdomlem3  9249  wemaplem2  9539  cantnfp1lem1  9670  cantnfp1lem2  9671  cantnfp1lem3  9672  cantnflem1d  9680  cantnflem1  9681  ssfzunsnext  13544  relexpsucnnr  14970  rexuzre  15297  rexico  15298  limsupgre  15423  rlim3  15440  o1lo1  15479  rlimclim1  15487  lo1resb  15506  o1resb  15508  o1of2  15555  o1rlimmul  15561  lo1le  15596  ruclem1  16173  ruclem10  16181  bitsfzo  16375  ramub1lem2  16961  ramcl  16963  prmocl  16968  prmop1  16972  prmdvdsprmo  16976  prmolefac  16980  prmodvdslcmf  16981  prmgapprmo  16996  setsstruct2  17108  wunress  17196  wunressOLD  17197  opifismgm  18584  mulgfval  18989  frgpuptf  19682  gsumzsplit  19839  gsummpt1n0  19877  xrsds  21274  uvcvvcl2  21653  uvcff  21656  snifpsrbag  21786  psr1cl  21834  subrgpsr  21851  mvrf  21856  mplmon  21902  mplmonmul  21903  mplcoe1  21904  evlslem3  21955  evlslem1  21957  coe1tmfv2  22118  gsummoncoe1  22151  mamumat1cl  22265  dmatmulcl  22326  scmatscmiddistr  22334  1mavmul  22374  marrepeval  22389  marrepcl  22390  marepveval  22394  marepvcl  22395  mdetrsca2  22430  mdetr0  22431  mdetrlin2  22433  mdetralt2  22435  mdetero  22436  mdetunilem2  22439  mdetunilem5  22442  mdetunilem6  22443  mdetunilem8  22445  mdetunilem9  22446  maducoeval2  22466  maduf  22467  madutpos  22468  madugsum  22469  gsummatr01lem3  22483  marep01ma  22486  smadiadetglem2  22498  monmatcollpw  22605  pmatcollpw3fi1lem1  22612  pmatcollpw3fi1lem2  22613  xkopt  23483  tsmssplit  23980  ssblex  24258  stdbdxmet  24348  stdbdmet  24349  stdbdbl  24350  stdbdmopn  24351  nlmvscnlem1  24527  tgioo  24636  xrsxmet  24649  icccmplem2  24663  ipcnlem1  25097  ivthlem2  25305  ovolicc2lem5  25374  ioombl1lem1  25411  ioombl1lem3  25413  ioombl1lem4  25414  mbfmax  25502  i1fres  25559  itg1climres  25568  mbfi1fseqlem3  25571  mbfi1fseqlem4  25572  mbfi1fseqlem5  25573  limcres  25739  dvferm1lem  25840  dvferm2lem  25842  dvlip2  25852  lhop1  25871  dvfsumrlim  25890  mdegaddle  25934  deg1addle2  25962  deg1sublt  25970  ply1divmo  25995  plyaddlem1  26069  plyaddlem  26071  coeaddlem  26105  dgradd2  26125  plydiveu  26154  abelthlem9  26296  logcnlem2  26496  logcnlem3  26497  cxpcn3lem  26601  lgamgulmlem4  26883  lgamgulmlem6  26885  ftalem2  26925  gausslemma2dlem4  27221  chebbnd1lem1  27321  dchrisumlem3  27343  dchrvmasumiflem1  27353  ostth3  27490  abssval  28052  absscl  28053  axlowdimlem15  28686  elrspunsn  33019  ply1moneq  33133  deg1addlt  33139  dstfrvunirn  33965  circlemeth  34143  indispconn  34716  ex-sategoelel  34903  ex-sategoelelomsuc  34908  knoppndvlem18  35896  itg2addnclem2  37034  itg2addnclem3  37035  ftc1anclem5  37059  sticksstones10  41468  sticksstones12a  41470  metakunt3  41484  metakunt4  41485  metakunt29  41510  metakunt30  41511  metakunt32  41513  metakunt33  41514  rhmmpl  41618  evlsbagval  41631  selvvvval  41650  fsuppind  41655  fsuppssind  41658  mhpind  41659  dffltz  41890  irrapxlem4  42077  irrapxlem5  42078  kelac1  42319  areaquad  42479  cantnfresb  42588  sqrtcval  42906  clsk1indlem4  43309  mnringmulrcld  43501  refsum2cnlem1  44235  rexabslelem  44638  uzublem  44650  ioondisj2  44716  ioondisj1  44717  uzubioo  44790  mullimc  44842  mullimcf  44849  lptioo2  44857  limcleqr  44870  0ellimcdiv  44875  limsupubuzlem  44938  limsupequzmptlem  44954  climxrre  44976  limsup10exlem  44998  limsup10ex  44999  liminf10ex  45000  liminflelimsuplem  45001  icccncfext  45113  cncfiooicclem1  45119  ioodvbdlimc1lem2  45158  ioodvbdlimc2lem  45160  stoweid  45289  fourierdlem9  45342  fourierdlem10  45343  fourierdlem37  45370  fourierdlem40  45373  fourierdlem66  45398  fourierdlem73  45405  fourierdlem74  45406  fourierdlem75  45407  fourierdlem78  45410  fourierdlem79  45411  fourierdlem95  45427  fourierdlem103  45435  sqwvfoura  45454  fouriersw  45457  etransclem1  45461  etransclem4  45464  etransclem17  45477  etransclem18  45478  etransclem19  45479  etransclem20  45480  etransclem21  45481  etransclem22  45482  etransclem23  45483  etransclem27  45487  etransclem32  45492  etransclem35  45495  etransclem46  45506  ioorrnopnlem  45530  ovnval2  45771  volicorecl  45772  hoiprodcl  45773  ovnf  45789  hsphoif  45802  hsphoival  45805  hoiprodcl3  45806  volicore  45807  hoidmvcl  45808  hsphoidmvle2  45811  hsphoidmvle  45812  hoidmv1lelem1  45817  hoidmv1lelem2  45818  hoidmv1lelem3  45819  hoidmvlelem2  45822  hoidmvlelem3  45823  ovnhoilem1  45827  hoidifhspf  45844  hoidifhspval3  45845  ovolval4lem1  45875  ovolval4lem2  45876  smfmullem1  46017  smfmullem2  46018  smfmullem3  46019  afv2ex  46432  suppmptcfin  47269  linc1  47319  lcoss  47330  el0ldep  47360