Theorem ifcld 4512

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

Syntax hints:   → wi 4   ∈ wcel 2114  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  soltmin  5996  pw2f1olem  8621  unxpdomlem3  8724  wemaplem2  9011  cantnfp1lem1  9141  cantnfp1lem2  9142  cantnfp1lem3  9143  cantnflem1d  9151  cantnflem1  9152  ssfzunsnext  12953  relexpsucnnr  14384  rexuzre  14712  rexico  14713  limsupgre  14838  rlim3  14855  o1lo1  14894  rlimclim1  14902  lo1resb  14921  o1resb  14923  o1of2  14969  o1rlimmul  14975  lo1le  15008  ruclem1  15584  ruclem10  15592  bitsfzo  15784  ramub1lem2  16363  ramcl  16365  prmocl  16370  prmop1  16374  prmdvdsprmo  16378  prmolefac  16382  prmodvdslcmf  16383  prmgapprmo  16398  setsstruct2  16521  wunress  16564  opifismgm  17869  mulgfval  18226  frgpuptf  18896  gsumzsplit  19047  gsummpt1n0  19085  snifpsrbag  20146  psr1cl  20182  subrgpsr  20199  mvrf  20204  mplmon  20244  mplmonmul  20245  mplcoe1  20246  evlslem3  20293  evlslem1  20295  coe1tmfv2  20443  gsummoncoe1  20472  xrsds  20588  uvcvvcl2  20932  uvcff  20935  mamumat1cl  21048  dmatmulcl  21109  scmatscmiddistr  21117  1mavmul  21157  marrepeval  21172  marrepcl  21173  marepveval  21177  marepvcl  21178  mdetrsca2  21213  mdetr0  21214  mdetrlin2  21216  mdetralt2  21218  mdetero  21219  mdetunilem2  21222  mdetunilem5  21225  mdetunilem6  21226  mdetunilem8  21228  mdetunilem9  21229  maducoeval2  21249  maduf  21250  madutpos  21251  madugsum  21252  gsummatr01lem3  21266  marep01ma  21269  smadiadetglem2  21281  monmatcollpw  21387  pmatcollpw3fi1lem1  21394  pmatcollpw3fi1lem2  21395  xkopt  22263  tsmssplit  22760  ssblex  23038  stdbdxmet  23125  stdbdmet  23126  stdbdbl  23127  stdbdmopn  23128  nlmvscnlem1  23295  tgioo  23404  xrsxmet  23417  icccmplem2  23431  ipcnlem1  23848  ivthlem2  24053  ovolicc2lem5  24122  ioombl1lem1  24159  ioombl1lem3  24161  ioombl1lem4  24162  mbfmax  24250  i1fres  24306  itg1climres  24315  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  limcres  24484  dvferm1lem  24581  dvferm2lem  24583  dvlip2  24592  lhop1  24611  dvfsumrlim  24628  mdegaddle  24668  deg1addle2  24696  deg1sublt  24704  ply1divmo  24729  plyaddlem1  24803  plyaddlem  24805  coeaddlem  24839  dgradd2  24858  plydiveu  24887  abelthlem9  25028  logcnlem2  25226  logcnlem3  25227  cxpcn3lem  25328  lgamgulmlem4  25609  lgamgulmlem6  25611  ftalem2  25651  gausslemma2dlem4  25945  chebbnd1lem1  26045  dchrisumlem3  26067  dchrvmasumiflem1  26077  ostth3  26214  axlowdimlem15  26742  dstfrvunirn  31732  circlemeth  31911  indispconn  32481  ex-sategoelel  32668  ex-sategoelelomsuc  32673  noprefixmo  33202  knoppndvlem18  33868  itg2addnclem2  34959  itg2addnclem3  34960  ftc1anclem5  34986  dffltz  39320  irrapxlem4  39471  irrapxlem5  39472  kelac1  39712  areaquad  39872  clsk1indlem4  40443  refsum2cnlem1  41343  rexabslelem  41741  uzublem  41753  ioondisj2  41816  ioondisj1  41817  uzubioo  41892  mullimc  41946  mullimcf  41953  lptioo2  41961  limcleqr  41974  0ellimcdiv  41979  limsupubuzlem  42042  limsupequzmptlem  42058  climxrre  42080  limsup10exlem  42102  limsup10ex  42103  liminf10ex  42104  liminflelimsuplem  42105  icccncfext  42219  cncfiooicclem1  42225  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  stoweid  42397  fourierdlem9  42450  fourierdlem10  42451  fourierdlem37  42478  fourierdlem40  42481  fourierdlem66  42506  fourierdlem73  42513  fourierdlem74  42514  fourierdlem75  42515  fourierdlem78  42518  fourierdlem79  42519  fourierdlem95  42535  fourierdlem103  42543  sqwvfoura  42562  fouriersw  42565  etransclem1  42569  etransclem4  42572  etransclem17  42585  etransclem18  42586  etransclem19  42587  etransclem20  42588  etransclem21  42589  etransclem22  42590  etransclem23  42591  etransclem27  42595  etransclem32  42600  etransclem35  42603  etransclem46  42614  ioorrnopnlem  42638  ovnval2  42876  volicorecl  42877  hoiprodcl  42878  ovnf  42894  hsphoif  42907  hsphoival  42910  hoiprodcl3  42911  volicore  42912  hoidmvcl  42913  hsphoidmvle2  42916  hsphoidmvle  42917  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmvlelem2  42927  hoidmvlelem3  42928  ovnhoilem1  42932  hoidifhspf  42949  hoidifhspval3  42950  ovolval4lem1  42980  ovolval4lem2  42981  smfmullem1  43115  smfmullem2  43116  smfmullem3  43117  afv2ex  43462  suppmptcfin  44476  linc1  44529  lcoss  44540  el0ldep  44570