Theorem ifcld 4536

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ifcif 4489

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  ifexd  4538  soltmin  6138  pw2f1olem  9076  unxpdomlem3  9225  wemaplem2  9516  cantnfp1lem1  9654  cantnfp1lem2  9655  cantnfp1lem3  9656  cantnflem1d  9664  cantnflem1  9665  ssfzunsnext  13618  tpf  14558  relexpsucnnr  15090  rexuzre  15432  rexico  15433  limsupgre  15560  rlim3  15577  o1lo1  15616  rlimclim1  15624  lo1resb  15643  o1resb  15645  o1of2  15692  o1rlimmul  15698  lo1le  15731  ruclem1  16313  ruclem10  16321  bitsfzo  16519  ramub1lem2  17113  ramcl  17115  prmocl  17120  prmop1  17124  prmdvdsprmo  17128  prmolefac  17132  prmodvdslcmf  17133  prmgapprmo  17148  setsstruct2  17260  wunress  17335  opifismgm  18745  mulgfval  19183  frgpuptf  19888  gsumzsplit  20045  gsummpt1n0  20083  xrsds  21614  uvcvvcl2  21992  uvcff  21995  snifpsrbag  22124  psr1cl  22164  subrgpsr  22181  mvrf  22188  mplmon  22240  mplmonmul  22241  mplcoe1  22242  evlslem3  22285  evlslem1  22287  selvvvval  22347  coe1tmfv2  22490  gsummoncoe1  22522  rhmmpl  22594  rhmply1vr1  22598  mamumat1cl  22650  dmatmulcl  22711  scmatscmiddistr  22719  1mavmul  22759  marrepeval  22774  marrepcl  22775  marepveval  22779  marepvcl  22780  mdetrsca2  22815  mdetr0  22816  mdetrlin2  22818  mdetralt2  22820  mdetero  22821  mdetunilem2  22824  mdetunilem5  22827  mdetunilem6  22828  mdetunilem8  22830  mdetunilem9  22831  maducoeval2  22851  maduf  22852  madutpos  22853  madugsum  22854  gsummatr01lem3  22868  marep01ma  22871  smadiadetglem2  22883  monmatcollpw  22990  pmatcollpw3fi1lem1  22997  pmatcollpw3fi1lem2  22998  xkopt  23867  tsmssplit  24364  ssblex  24640  stdbdxmet  24727  stdbdmet  24728  stdbdbl  24729  stdbdmopn  24730  nlmvscnlem1  24898  tgioo  25008  xrsxmet  25022  icccmplem2  25036  ipcnlem1  25459  ivthlem2  25666  ovolicc2lem5  25735  ioombl1lem1  25772  ioombl1lem3  25774  ioombl1lem4  25775  mbfmax  25863  i1fres  25919  itg1climres  25928  mbfi1fseqlem3  25931  mbfi1fseqlem4  25932  mbfi1fseqlem5  25933  limcres  26100  dvferm1lem  26198  dvferm2lem  26200  dvlip2  26209  lhop1  26228  dvfsumrlim  26245  mdegaddle  26286  deg1addle2  26314  deg1sublt  26322  ply1divmo  26348  plyaddlem1  26425  plyaddlem  26427  coeaddlem  26461  dgradd2  26480  plydiveu  26514  abelthlem9  26658  logcnlem2  26863  logcnlem3  26864  cxpcn3lem  26967  lgamgulmlem4  27251  lgamgulmlem6  27253  ftalem2  27293  gausslemma2dlem4  27588  chebbnd1lem1  27688  dchrisumlem3  27710  dchrvmasumiflem1  27720  ostth3  27857  abssval  28487  absscl  28488  axlowdimlem15  29365  elrspunsn  33805  ply1moneq  33946  deg1addlt  33958  mplasclco  33974  selvply1rhmlem2  33979  extvfvv  33992  extvfvvcl  33993  extvfvcl  33994  mplvrpmrhm  34005  psrmon  34007  psrmonmul  34008  psrmonprod  34010  mplmonprod  34012  esplyfval0  34022  esplyfval1  34031  esplyind  34033  fldextrspunlsp  34132  dstfrvunirn  34934  circlemeth  35096  indispconn  35767  ex-sategoelel  35954  ex-sategoelelomsuc  35959  knoppndvlem18  37179  itg2addnclem2  38384  itg2addnclem3  38385  ftc1anclem5  38409  sticksstones10  42984  sticksstones12a  42986  aks6d1c6lem3  43001  rhmpsr  43392  evlsbagval  43395  fsuppind  43399  fsuppssind  43402  mhpind  43403  dffltz  43443  irrapxlem4  43629  irrapxlem5  43630  kelac1  43867  areaquad  44020  cantnfresb  44128  sqrtcval  44444  clsk1indlem4  44847  mnringmulrcld  45029  refsum2cnlem1  45834  rexabslelem  46209  uzublem  46221  ioondisj2  46286  ioondisj1  46287  uzubioo  46358  mullimc  46409  mullimcf  46416  lptioo2  46424  limcleqr  46435  0ellimcdiv  46440  limsupubuzlem  46503  limsupequzmptlem  46519  climxrre  46541  limsup10exlem  46563  limsup10ex  46564  liminf10ex  46565  liminflelimsuplem  46566  icccncfext  46678  cncfiooicclem1  46684  ioodvbdlimc1lem2  46723  ioodvbdlimc2lem  46725  stoweid  46854  fourierdlem9  46907  fourierdlem10  46908  fourierdlem37  46935  fourierdlem40  46938  fourierdlem66  46963  fourierdlem73  46970  fourierdlem74  46971  fourierdlem75  46972  fourierdlem78  46975  fourierdlem79  46976  fourierdlem95  46992  fourierdlem103  47000  sqwvfoura  47019  fouriersw  47022  etransclem1  47026  etransclem4  47029  etransclem17  47042  etransclem18  47043  etransclem19  47044  etransclem20  47045  etransclem21  47046  etransclem22  47047  etransclem23  47048  etransclem27  47052  etransclem32  47057  etransclem35  47060  etransclem46  47071  ioorrnopnlem  47095  ovnval2  47336  volicorecl  47337  hoiprodcl  47338  ovnf  47354  hsphoif  47367  hsphoival  47370  hoiprodcl3  47371  volicore  47372  hoidmvcl  47373  hsphoidmvle2  47376  hsphoidmvle  47377  hoidmv1lelem1  47382  hoidmv1lelem2  47383  hoidmv1lelem3  47384  hoidmvlelem2  47387  hoidmvlelem3  47388  ovnhoilem1  47392  hoidifhspf  47409  hoidifhspval3  47410  ovolval4lem1  47440  ovolval4lem2  47441  smfmullem1  47582  smfmullem2  47583  smfmullem3  47584  afv2ex  48028  suppmptcfin  49232  linc1  49281  lcoss  49292  el0ldep  49322  crosspclem  50716