Theorem ifcld 4081

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

Syntax hints:   → wi 4   ∈ wcel 1977  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  soltmin  5451  pw2f1olem  7949  unxpdomlem3  8051  wemaplem2  8335  cantnfp1lem1  8458  cantnfp1lem2  8459  cantnfp1lem3  8460  cantnflem1d  8468  cantnflem1  8469  ssfzunsn  12257  relexpsucnnr  13613  rexuzre  13940  rexico  13941  limsupgre  14060  rlim3  14077  o1lo1  14116  rlimclim1  14124  lo1resb  14143  o1resb  14145  o1of2  14191  o1rlimmul  14197  lo1le  14230  ruclem1  14799  ruclem10  14807  bitsfzo  14995  ramub1lem2  15569  ramcl  15571  prmocl  15576  prmop1  15580  prmdvdsprmo  15584  prmolefac  15588  prmodvdslcmf  15589  prmgapprmo  15604  setsstruct  15727  wunress  15767  opifismgm  17081  frgpuptf  18006  gsumzsplit  18150  gsummpt1n0  18187  snifpsrbag  19187  psr1cl  19223  subrgpsr  19240  mvrf  19245  mplmon  19284  mplmonmul  19285  mplcoe1  19286  evlslem3  19335  evlslem1  19336  coe1tmfv2  19466  gsummoncoe1  19495  xrsds  19608  uvcvvcl2  19946  uvcff  19949  mamumat1cl  20064  dmatmulcl  20125  scmatscmiddistr  20133  1mavmul  20173  marrepeval  20188  marrepcl  20189  marepveval  20193  marepvcl  20194  mdetrsca2  20229  mdetr0  20230  mdetrlin2  20232  mdetralt2  20234  mdetero  20235  mdetunilem2  20238  mdetunilem5  20241  mdetunilem6  20242  mdetunilem8  20244  mdetunilem9  20245  maducoeval2  20265  maduf  20266  madutpos  20267  madugsum  20268  gsummatr01lem3  20282  marep01ma  20285  smadiadetglem2  20297  monmatcollpw  20403  pmatcollpw3fi1lem1  20410  pmatcollpw3fi1lem2  20411  xkopt  21268  tsmssplit  21765  ssblex  22043  stdbdxmet  22130  stdbdmet  22131  stdbdbl  22132  stdbdmopn  22133  nlmvscnlem1  22300  tgioo  22407  xrsxmet  22420  icccmplem2  22434  ipcnlem1  22852  ivthlem2  23028  ovolicc2lem5  23096  ioombl1lem1  23133  ioombl1lem3  23135  ioombl1lem4  23136  mbfmax  23222  i1fres  23278  itg1climres  23287  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  limcres  23456  dvferm1lem  23551  dvferm2lem  23553  dvlip2  23562  lhop1  23581  dvfsumrlim  23598  mdegaddle  23638  deg1addle2  23666  deg1sublt  23674  ply1divmo  23699  plyaddlem1  23773  plyaddlem  23775  coeaddlem  23809  dgradd2  23828  plydiveu  23857  abelthlem9  23998  logcnlem2  24189  logcnlem3  24190  cxpcn3lem  24288  lgamgulmlem4  24558  lgamgulmlem6  24560  ftalem2  24600  gausslemma2dlem4  24894  chebbnd1lem1  24958  dchrisumlem3  24980  dchrvmasumiflem1  24990  ostth3  25127  axlowdimlem15  25636  dstfrvunirn  29863  indispcon  30470  knoppndvlem18  31690  itg2addnclem2  32632  itg2addnclem3  32633  ftc1anclem5  32659  irrapxlem4  36407  irrapxlem5  36408  kelac1  36651  areaquad  36821  clsk1indlem4  37362  refsum2cnlem1  38219  ioondisj2  38561  ioondisj1  38562  mullimc  38683  mullimcf  38690  lptioo2  38698  limcleqr  38711  0ellimcdiv  38716  icccncfext  38773  cncfiooicclem1  38779  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweid  38956  fourierdlem9  39009  fourierdlem10  39010  fourierdlem37  39037  fourierdlem40  39040  fourierdlem66  39065  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem78  39077  fourierdlem79  39078  fourierdlem95  39094  fourierdlem103  39102  sqwvfoura  39121  fouriersw  39124  etransclem1  39128  etransclem4  39131  etransclem17  39144  etransclem18  39145  etransclem19  39146  etransclem20  39147  etransclem21  39148  etransclem22  39149  etransclem23  39150  etransclem27  39154  etransclem32  39159  etransclem35  39162  etransclem46  39173  ioorrnopnlem  39200  ovnval2  39435  volicorecl  39436  hoiprodcl  39437  ovnf  39453  hsphoif  39466  hsphoival  39469  hoiprodcl3  39470  volicore  39471  hoidmvcl  39472  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem1  39491  hoidifhspf  39508  hoidifhspval3  39509  ovolval4lem1  39539  ovolval4lem2  39540  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  suppmptcfin  41954  linc1  42008  lcoss  42019  el0ldep  42049