Theorem ifcld 4574

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

Syntax hints:   → wi 4   ∈ wcel 2107  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  ifexd  4576  soltmin  6135  pw2f1olem  9073  unxpdomlem3  9249  wemaplem2  9539  cantnfp1lem1  9670  cantnfp1lem2  9671  cantnfp1lem3  9672  cantnflem1d  9680  cantnflem1  9681  ssfzunsnext  13543  relexpsucnnr  14969  rexuzre  15296  rexico  15297  limsupgre  15422  rlim3  15439  o1lo1  15478  rlimclim1  15486  lo1resb  15505  o1resb  15507  o1of2  15554  o1rlimmul  15560  lo1le  15595  ruclem1  16171  ruclem10  16179  bitsfzo  16373  ramub1lem2  16957  ramcl  16959  prmocl  16964  prmop1  16968  prmdvdsprmo  16972  prmolefac  16976  prmodvdslcmf  16977  prmgapprmo  16992  setsstruct2  17104  wunress  17192  wunressOLD  17193  opifismgm  18575  mulgfval  18947  frgpuptf  19633  gsumzsplit  19790  gsummpt1n0  19828  xrsds  20981  uvcvvcl2  21335  uvcff  21338  snifpsrbag  21467  psr1cl  21514  subrgpsr  21531  mvrf  21536  mplmon  21582  mplmonmul  21583  mplcoe1  21584  evlslem3  21635  evlslem1  21637  coe1tmfv2  21789  gsummoncoe1  21820  mamumat1cl  21933  dmatmulcl  21994  scmatscmiddistr  22002  1mavmul  22042  marrepeval  22057  marrepcl  22058  marepveval  22062  marepvcl  22063  mdetrsca2  22098  mdetr0  22099  mdetrlin2  22101  mdetralt2  22103  mdetero  22104  mdetunilem2  22107  mdetunilem5  22110  mdetunilem6  22111  mdetunilem8  22113  mdetunilem9  22114  maducoeval2  22134  maduf  22135  madutpos  22136  madugsum  22137  gsummatr01lem3  22151  marep01ma  22154  smadiadetglem2  22166  monmatcollpw  22273  pmatcollpw3fi1lem1  22280  pmatcollpw3fi1lem2  22281  xkopt  23151  tsmssplit  23648  ssblex  23926  stdbdxmet  24016  stdbdmet  24017  stdbdbl  24018  stdbdmopn  24019  nlmvscnlem1  24195  tgioo  24304  xrsxmet  24317  icccmplem2  24331  ipcnlem1  24754  ivthlem2  24961  ovolicc2lem5  25030  ioombl1lem1  25067  ioombl1lem3  25069  ioombl1lem4  25070  mbfmax  25158  i1fres  25215  itg1climres  25224  mbfi1fseqlem3  25227  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  limcres  25395  dvferm1lem  25493  dvferm2lem  25495  dvlip2  25504  lhop1  25523  dvfsumrlim  25540  mdegaddle  25584  deg1addle2  25612  deg1sublt  25620  ply1divmo  25645  plyaddlem1  25719  plyaddlem  25721  coeaddlem  25755  dgradd2  25774  plydiveu  25803  abelthlem9  25944  logcnlem2  26143  logcnlem3  26144  cxpcn3lem  26245  lgamgulmlem4  26526  lgamgulmlem6  26528  ftalem2  26568  gausslemma2dlem4  26862  chebbnd1lem1  26962  dchrisumlem3  26984  dchrvmasumiflem1  26994  ostth3  27131  axlowdimlem15  28204  elrspunsn  32536  ply1moneq  32654  dstfrvunirn  33462  circlemeth  33641  indispconn  34214  ex-sategoelel  34401  ex-sategoelelomsuc  34406  knoppndvlem18  35394  itg2addnclem2  36529  itg2addnclem3  36530  ftc1anclem5  36554  sticksstones10  40960  sticksstones12a  40962  metakunt3  40976  metakunt4  40977  metakunt29  41002  metakunt30  41003  metakunt32  41005  metakunt33  41006  rhmmpl  41123  evlsbagval  41136  selvvvval  41155  fsuppind  41160  fsuppssind  41163  mhpind  41164  dffltz  41373  irrapxlem4  41549  irrapxlem5  41550  kelac1  41791  areaquad  41951  cantnfresb  42060  sqrtcval  42378  clsk1indlem4  42781  mnringmulrcld  42973  refsum2cnlem1  43707  rexabslelem  44115  uzublem  44127  ioondisj2  44193  ioondisj1  44194  uzubioo  44267  mullimc  44319  mullimcf  44326  lptioo2  44334  limcleqr  44347  0ellimcdiv  44352  limsupubuzlem  44415  limsupequzmptlem  44431  climxrre  44453  limsup10exlem  44475  limsup10ex  44476  liminf10ex  44477  liminflelimsuplem  44478  icccncfext  44590  cncfiooicclem1  44596  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  stoweid  44766  fourierdlem9  44819  fourierdlem10  44820  fourierdlem37  44847  fourierdlem40  44850  fourierdlem66  44875  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem78  44887  fourierdlem79  44888  fourierdlem95  44904  fourierdlem103  44912  sqwvfoura  44931  fouriersw  44934  etransclem1  44938  etransclem4  44941  etransclem17  44954  etransclem18  44955  etransclem19  44956  etransclem20  44957  etransclem21  44958  etransclem22  44959  etransclem23  44960  etransclem27  44964  etransclem32  44969  etransclem35  44972  etransclem46  44983  ioorrnopnlem  45007  ovnval2  45248  volicorecl  45249  hoiprodcl  45250  ovnf  45266  hsphoif  45279  hsphoival  45282  hoiprodcl3  45283  volicore  45284  hoidmvcl  45285  hsphoidmvle2  45288  hsphoidmvle  45289  hoidmv1lelem1  45294  hoidmv1lelem2  45295  hoidmv1lelem3  45296  hoidmvlelem2  45299  hoidmvlelem3  45300  ovnhoilem1  45304  hoidifhspf  45321  hoidifhspval3  45322  ovolval4lem1  45352  ovolval4lem2  45353  smfmullem1  45494  smfmullem2  45495  smfmullem3  45496  afv2ex  45909  suppmptcfin  47009  linc1  47060  lcoss  47071  el0ldep  47101