Theorem ifcld 4523

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

Syntax hints:   → wi 4   ∈ wcel 2109  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4477

This theorem is referenced by:  ifexd  4525  soltmin  6085  pw2f1olem  8998  unxpdomlem3  9147  wemaplem2  9439  cantnfp1lem1  9574  cantnfp1lem2  9575  cantnfp1lem3  9576  cantnflem1d  9584  cantnflem1  9585  ssfzunsnext  13472  tpf  14406  relexpsucnnr  14932  rexuzre  15260  rexico  15261  limsupgre  15388  rlim3  15405  o1lo1  15444  rlimclim1  15452  lo1resb  15471  o1resb  15473  o1of2  15520  o1rlimmul  15526  lo1le  15559  ruclem1  16140  ruclem10  16148  bitsfzo  16346  ramub1lem2  16939  ramcl  16941  prmocl  16946  prmop1  16950  prmdvdsprmo  16954  prmolefac  16958  prmodvdslcmf  16959  prmgapprmo  16974  setsstruct2  17085  wunress  17160  opifismgm  18533  mulgfval  18948  frgpuptf  19649  gsumzsplit  19806  gsummpt1n0  19844  xrsds  21316  uvcvvcl2  21695  uvcff  21698  snifpsrbag  21827  psr1cl  21868  subrgpsr  21885  mvrf  21892  mplmon  21940  mplmonmul  21941  mplcoe1  21942  evlslem3  21985  evlslem1  21987  coe1tmfv2  22159  gsummoncoe1  22193  rhmmpl  22268  rhmply1vr1  22272  mamumat1cl  22324  dmatmulcl  22385  scmatscmiddistr  22393  1mavmul  22433  marrepeval  22448  marrepcl  22449  marepveval  22453  marepvcl  22454  mdetrsca2  22489  mdetr0  22490  mdetrlin2  22492  mdetralt2  22494  mdetero  22495  mdetunilem2  22498  mdetunilem5  22501  mdetunilem6  22502  mdetunilem8  22504  mdetunilem9  22505  maducoeval2  22525  maduf  22526  madutpos  22527  madugsum  22528  gsummatr01lem3  22542  marep01ma  22545  smadiadetglem2  22557  monmatcollpw  22664  pmatcollpw3fi1lem1  22671  pmatcollpw3fi1lem2  22672  xkopt  23540  tsmssplit  24037  ssblex  24314  stdbdxmet  24401  stdbdmet  24402  stdbdbl  24403  stdbdmopn  24404  nlmvscnlem1  24572  tgioo  24682  xrsxmet  24696  icccmplem2  24710  ipcnlem1  25143  ivthlem2  25351  ovolicc2lem5  25420  ioombl1lem1  25457  ioombl1lem3  25459  ioombl1lem4  25460  mbfmax  25548  i1fres  25604  itg1climres  25613  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  limcres  25785  dvferm1lem  25886  dvferm2lem  25888  dvlip2  25898  lhop1  25917  dvfsumrlim  25936  mdegaddle  25977  deg1addle2  26005  deg1sublt  26013  ply1divmo  26039  plyaddlem1  26116  plyaddlem  26118  coeaddlem  26152  dgradd2  26172  plydiveu  26204  abelthlem9  26348  logcnlem2  26550  logcnlem3  26551  cxpcn3lem  26655  lgamgulmlem4  26940  lgamgulmlem6  26942  ftalem2  26982  gausslemma2dlem4  27278  chebbnd1lem1  27378  dchrisumlem3  27400  dchrvmasumiflem1  27410  ostth3  27547  abssval  28146  absscl  28147  axlowdimlem15  28901  elrspunsn  33367  ply1moneq  33523  deg1addlt  33533  fldextrspunlsp  33647  dstfrvunirn  34449  circlemeth  34614  indispconn  35217  ex-sategoelel  35404  ex-sategoelelomsuc  35409  knoppndvlem18  36513  itg2addnclem2  37662  itg2addnclem3  37663  ftc1anclem5  37687  sticksstones10  42138  sticksstones12a  42140  aks6d1c6lem3  42155  rhmpsr  42535  evlsbagval  42549  selvvvval  42568  fsuppind  42573  fsuppssind  42576  mhpind  42577  dffltz  42617  irrapxlem4  42808  irrapxlem5  42809  kelac1  43046  areaquad  43199  cantnfresb  43307  sqrtcval  43624  clsk1indlem4  44027  mnringmulrcld  44211  refsum2cnlem1  45025  rexabslelem  45407  uzublem  45419  ioondisj2  45484  ioondisj1  45485  uzubioo  45556  mullimc  45607  mullimcf  45614  lptioo2  45622  limcleqr  45635  0ellimcdiv  45640  limsupubuzlem  45703  limsupequzmptlem  45719  climxrre  45741  limsup10exlem  45763  limsup10ex  45764  liminf10ex  45765  liminflelimsuplem  45766  icccncfext  45878  cncfiooicclem1  45884  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweid  46054  fourierdlem9  46107  fourierdlem10  46108  fourierdlem37  46135  fourierdlem40  46138  fourierdlem66  46163  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem78  46175  fourierdlem79  46176  fourierdlem95  46192  fourierdlem103  46200  sqwvfoura  46219  fouriersw  46222  etransclem1  46226  etransclem4  46229  etransclem17  46242  etransclem18  46243  etransclem19  46244  etransclem20  46245  etransclem21  46246  etransclem22  46247  etransclem23  46248  etransclem27  46252  etransclem32  46257  etransclem35  46260  etransclem46  46271  ioorrnopnlem  46295  ovnval2  46536  volicorecl  46537  hoiprodcl  46538  ovnf  46554  hsphoif  46567  hsphoival  46570  hoiprodcl3  46571  volicore  46572  hoidmvcl  46573  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnhoilem1  46592  hoidifhspf  46609  hoidifhspval3  46610  ovolval4lem1  46640  ovolval4lem2  46641  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  afv2ex  47208  suppmptcfin  48370  linc1  48420  lcoss  48431  el0ldep  48461