Theorem ifcld 4534

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  ifcif 4487

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4488

This theorem is used by:  ifexd  4536  soltmin  6136  pw2f1olem  9065  unxpdomlem3  9214  wemaplem2  9505  cantnfp1lem1  9643  cantnfp1lem2  9644  cantnfp1lem3  9645  cantnflem1d  9653  cantnflem1  9654  ssfzunsnext  13602  tpf  14541  relexpsucnnr  15067  rexuzre  15409  rexico  15410  limsupgre  15537  rlim3  15554  o1lo1  15593  rlimclim1  15601  lo1resb  15620  o1resb  15622  o1of2  15669  o1rlimmul  15675  lo1le  15708  ruclem1  16291  ruclem10  16299  bitsfzo  16497  ramub1lem2  17091  ramcl  17093  prmocl  17098  prmop1  17102  prmdvdsprmo  17106  prmolefac  17110  prmodvdslcmf  17111  prmgapprmo  17126  setsstruct2  17238  wunress  17313  opifismgm  18721  mulgfval  19139  frgpuptf  19844  gsumzsplit  20001  gsummpt1n0  20039  xrsds  21569  uvcvvcl2  21947  uvcff  21950  snifpsrbag  22079  psr1cl  22119  subrgpsr  22136  mvrf  22143  mplmon  22195  mplmonmul  22196  mplcoe1  22197  evlslem3  22240  evlslem1  22242  selvvvval  22302  coe1tmfv2  22445  gsummoncoe1  22477  rhmmpl  22549  rhmply1vr1  22553  mamumat1cl  22605  dmatmulcl  22666  scmatscmiddistr  22674  1mavmul  22714  marrepeval  22729  marrepcl  22730  marepveval  22734  marepvcl  22735  mdetrsca2  22770  mdetr0  22771  mdetrlin2  22773  mdetralt2  22775  mdetero  22776  mdetunilem2  22779  mdetunilem5  22782  mdetunilem6  22783  mdetunilem8  22785  mdetunilem9  22786  maducoeval2  22806  maduf  22807  madutpos  22808  madugsum  22809  gsummatr01lem3  22823  marep01ma  22826  smadiadetglem2  22838  monmatcollpw  22945  pmatcollpw3fi1lem1  22952  pmatcollpw3fi1lem2  22953  xkopt  23821  tsmssplit  24318  ssblex  24594  stdbdxmet  24681  stdbdmet  24682  stdbdbl  24683  stdbdmopn  24684  nlmvscnlem1  24852  tgioo  24962  xrsxmet  24976  icccmplem2  24990  ipcnlem1  25413  ivthlem2  25620  ovolicc2lem5  25689  ioombl1lem1  25726  ioombl1lem3  25728  ioombl1lem4  25729  mbfmax  25817  i1fres  25873  itg1climres  25882  mbfi1fseqlem3  25885  mbfi1fseqlem4  25886  mbfi1fseqlem5  25887  limcres  26054  dvferm1lem  26152  dvferm2lem  26154  dvlip2  26163  lhop1  26182  dvfsumrlim  26199  mdegaddle  26240  deg1addle2  26268  deg1sublt  26276  ply1divmo  26302  plyaddlem1  26379  plyaddlem  26381  coeaddlem  26415  dgradd2  26434  plydiveu  26468  abelthlem9  26612  logcnlem2  26817  logcnlem3  26818  cxpcn3lem  26921  lgamgulmlem4  27205  lgamgulmlem6  27207  ftalem2  27247  gausslemma2dlem4  27542  chebbnd1lem1  27642  dchrisumlem3  27664  dchrvmasumiflem1  27674  ostth3  27811  abssval  28441  absscl  28442  axlowdimlem15  29315  elrspunsn  33746  ply1moneq  33887  deg1addlt  33899  mplasclco  33915  selvply1rhmlem2  33920  extvfvv  33933  extvfvvcl  33934  extvfvcl  33935  mplvrpmrhm  33946  psrmon  33948  psrmonmul  33949  psrmonprod  33951  mplmonprod  33953  esplyfval0  33963  esplyfval1  33972  esplyind  33974  fldextrspunlsp  34073  dstfrvunirn  34874  circlemeth  35036  indispconn  35734  ex-sategoelel  35921  ex-sategoelelomsuc  35926  knoppndvlem18  37146  itg2addnclem2  38351  itg2addnclem3  38352  ftc1anclem5  38376  sticksstones10  42950  sticksstones12a  42952  aks6d1c6lem3  42967  rhmpsr  43343  evlsbagval  43346  fsuppind  43350  fsuppssind  43353  mhpind  43354  dffltz  43394  irrapxlem4  43580  irrapxlem5  43581  kelac1  43818  areaquad  43971  cantnfresb  44079  sqrtcval  44395  clsk1indlem4  44798  mnringmulrcld  44980  refsum2cnlem1  45785  rexabslelem  46160  uzublem  46172  ioondisj2  46237  ioondisj1  46238  uzubioo  46309  mullimc  46360  mullimcf  46367  lptioo2  46375  limcleqr  46386  0ellimcdiv  46391  limsupubuzlem  46454  limsupequzmptlem  46470  climxrre  46492  limsup10exlem  46514  limsup10ex  46515  liminf10ex  46516  liminflelimsuplem  46517  icccncfext  46629  cncfiooicclem1  46635  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  stoweid  46805  fourierdlem9  46858  fourierdlem10  46859  fourierdlem37  46886  fourierdlem40  46889  fourierdlem66  46914  fourierdlem73  46921  fourierdlem74  46922  fourierdlem75  46923  fourierdlem78  46926  fourierdlem79  46927  fourierdlem95  46943  fourierdlem103  46951  sqwvfoura  46970  fouriersw  46973  etransclem1  46977  etransclem4  46980  etransclem17  46993  etransclem18  46994  etransclem19  46995  etransclem20  46996  etransclem21  46997  etransclem22  46998  etransclem23  46999  etransclem27  47003  etransclem32  47008  etransclem35  47011  etransclem46  47022  ioorrnopnlem  47046  ovnval2  47287  volicorecl  47288  hoiprodcl  47289  ovnf  47305  hsphoif  47318  hsphoival  47321  hoiprodcl3  47322  volicore  47323  hoidmvcl  47324  hsphoidmvle2  47327  hsphoidmvle  47328  hoidmv1lelem1  47333  hoidmv1lelem2  47334  hoidmv1lelem3  47335  hoidmvlelem2  47338  hoidmvlelem3  47339  ovnhoilem1  47343  hoidifhspf  47360  hoidifhspval3  47361  ovolval4lem1  47391  ovolval4lem2  47392  smfmullem1  47533  smfmullem2  47534  smfmullem3  47535  afv2ex  47979  suppmptcfin  49184  linc1  49233  lcoss  49244  el0ldep  49274