Theorem ifcld 4529

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  ifexd  4531  soltmin  6130  pw2f1olem  9082  unxpdomlem3  9231  wemaplem2  9522  cantnfp1lem1  9660  cantnfp1lem2  9661  cantnfp1lem3  9662  cantnflem1d  9670  cantnflem1  9671  ssfzunsnext  13627  tpf  14567  relexpsucnnr  15101  rexuzre  15443  rexico  15444  limsupgre  15571  rlim3  15588  o1lo1  15627  rlimclim1  15635  lo1resb  15654  o1resb  15656  o1of2  15703  o1rlimmul  15709  lo1le  15742  ruclem1  16322  ruclem10  16330  bitsfzo  16528  ramub1lem2  17122  ramcl  17124  prmocl  17129  prmop1  17133  prmdvdsprmo  17137  prmolefac  17141  prmodvdslcmf  17142  prmgapprmo  17157  setsstruct2  17269  wunress  17344  opifismgm  18754  mulgfval  19195  frgpuptf  19900  gsumzsplit  20057  gsummpt1n0  20095  xrsds  21626  uvcvvcl2  22004  uvcff  22007  snifpsrbag  22138  psr1cl  22178  subrgpsr  22195  mvrf  22202  mplmon  22254  mplmonmul  22255  mplcoe1  22256  evlslem3  22299  evlslem1  22301  selvvvval  22361  coe1tmfv2  22504  gsummoncoe1  22536  rhmmpl  22608  rhmply1vr1  22612  mamumat1cl  22664  dmatmulcl  22725  scmatscmiddistr  22733  1mavmul  22773  marrepeval  22788  marrepcl  22789  marepveval  22793  marepvcl  22794  mdetrsca2  22829  mdetr0  22830  mdetrlin2  22832  mdetralt2  22834  mdetero  22835  mdetunilem2  22838  mdetunilem5  22841  mdetunilem6  22842  mdetunilem8  22844  mdetunilem9  22845  maducoeval2  22865  maduf  22866  madutpos  22867  madugsum  22868  gsummatr01lem3  22882  marep01ma  22885  smadiadetglem2  22897  monmatcollpw  23007  pmatcollpw3fi1lem1  23014  pmatcollpw3fi1lem2  23015  xkopt  23884  tsmssplit  24381  ssblex  24657  stdbdxmet  24744  stdbdmet  24745  stdbdbl  24746  stdbdmopn  24747  nlmvscnlem1  24915  tgioo  25025  xrsxmet  25039  icccmplem2  25053  ipcnlem1  25476  ivthlem2  25683  ovolicc2lem5  25752  ioombl1lem1  25789  ioombl1lem3  25791  ioombl1lem4  25792  mbfmax  25880  i1fres  25936  itg1climres  25945  mbfi1fseqlem3  25948  mbfi1fseqlem4  25949  mbfi1fseqlem5  25950  limcres  26116  dvferm1lem  26214  dvferm2lem  26216  dvlip2  26225  lhop1  26244  dvfsumrlim  26261  mdegaddle  26302  deg1addle2  26330  deg1sublt  26338  ply1divmo  26364  plyaddlem1  26442  plyaddlem  26444  coeaddlem  26478  dgradd2  26497  plydiveu  26531  abelthlem9  26679  logcnlem2  26883  logcnlem3  26884  cxpcn3lem  26987  lgamgulmlem4  27271  lgamgulmlem6  27273  ftalem2  27313  gausslemma2dlem4  27608  chebbnd1lem1  27708  dchrisumlem3  27730  dchrvmasumiflem1  27740  ostth3  27877  abssval  28507  absscl  28508  axlowdimlem15  29416  elrspunsn  33860  ply1moneq  34001  deg1addlt  34013  mplasclco  34029  selvply1rhmlem2  34034  extvfvv  34047  extvfvvcl  34048  extvfvcl  34049  mplvrpmrhm  34060  psrmon  34062  psrmonmul  34063  psrmonprod  34065  mplmonprod  34067  esplyfval0  34077  esplyfval1  34086  esplyind  34088  fldextrspunlsp  34187  dstfrvunirn  34989  circlemeth  35151  indispconn  35816  ex-sategoelel  36003  ex-sategoelelomsuc  36008  knoppndvlem18  37229  itg2addnclem2  38424  itg2addnclem3  38425  ftc1anclem5  38449  sticksstones10  43024  sticksstones12a  43026  aks6d1c6lem3  43041  rhmpsr  43432  evlsbagval  43435  fsuppind  43439  fsuppssind  43442  mhpind  43443  dffltz  43483  irrapxlem4  43669  irrapxlem5  43670  kelac1  43907  areaquad  44060  cantnfresb  44168  sqrtcval  44484  clsk1indlem4  44887  mnringmulrcld  45069  refsum2cnlem1  45874  rexabslelem  46249  uzublem  46261  ioondisj2  46326  ioondisj1  46327  uzubioo  46398  mullimc  46449  mullimcf  46456  lptioo2  46464  limcleqr  46475  0ellimcdiv  46480  limsupubuzlem  46543  limsupequzmptlem  46559  climxrre  46581  limsup10exlem  46603  limsup10ex  46604  liminf10ex  46605  liminflelimsuplem  46606  icccncfext  46718  cncfiooicclem1  46724  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  stoweid  46894  fourierdlem9  46947  fourierdlem10  46948  fourierdlem37  46975  fourierdlem40  46978  fourierdlem66  47003  fourierdlem73  47010  fourierdlem74  47011  fourierdlem75  47012  fourierdlem78  47015  fourierdlem79  47016  fourierdlem95  47032  fourierdlem103  47040  sqwvfoura  47059  fouriersw  47062  etransclem1  47066  etransclem4  47069  etransclem17  47082  etransclem18  47083  etransclem19  47084  etransclem20  47085  etransclem21  47086  etransclem22  47087  etransclem23  47088  etransclem27  47092  etransclem32  47097  etransclem35  47100  etransclem46  47111  ioorrnopnlem  47135  ovnval2  47376  volicorecl  47377  hoiprodcl  47378  ovnf  47394  hsphoif  47407  hsphoival  47410  hoiprodcl3  47411  volicore  47412  hoidmvcl  47413  hsphoidmvle2  47416  hsphoidmvle  47417  hoidmv1lelem1  47422  hoidmv1lelem2  47423  hoidmv1lelem3  47424  hoidmvlelem2  47427  hoidmvlelem3  47428  ovnhoilem1  47432  hoidifhspf  47449  hoidifhspval3  47450  ovolval4lem1  47480  ovolval4lem2  47481  smfmullem1  47622  smfmullem2  47623  smfmullem3  47624  tmachlem-agreeprod  47768  tmachlem-tpopen  47772  afv2ex  48105  suppmptcfin  49309  linc1  49358  lcoss  49369  el0ldep  49399  crosspclem  50794  veronesefvcl  50808