MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifcld Structured version   Visualization version   GIF version

Theorem ifcld 4164
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
StepHypRef Expression
1 ifcld.a . 2 (𝜑𝐴𝐶)
2 ifcld.b . 2 (𝜑𝐵𝐶)
3 ifcl 4163 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3syl2anc 694 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120
This theorem is referenced by:  soltmin  5567  pw2f1olem  8105  unxpdomlem3  8207  wemaplem2  8493  cantnfp1lem1  8613  cantnfp1lem2  8614  cantnfp1lem3  8615  cantnflem1d  8623  cantnflem1  8624  ssfzunsnext  12424  relexpsucnnr  13809  rexuzre  14136  rexico  14137  limsupgre  14256  rlim3  14273  o1lo1  14312  rlimclim1  14320  lo1resb  14339  o1resb  14341  o1of2  14387  o1rlimmul  14393  lo1le  14426  ruclem1  15004  ruclem10  15012  bitsfzo  15204  ramub1lem2  15778  ramcl  15780  prmocl  15785  prmop1  15789  prmdvdsprmo  15793  prmolefac  15797  prmodvdslcmf  15798  prmgapprmo  15813  setsstruct2  15943  setsstructOLD  15946  wunress  15987  opifismgm  17305  frgpuptf  18229  gsumzsplit  18373  gsummpt1n0  18410  snifpsrbag  19414  psr1cl  19450  subrgpsr  19467  mvrf  19472  mplmon  19511  mplmonmul  19512  mplcoe1  19513  evlslem3  19562  evlslem1  19563  coe1tmfv2  19693  gsummoncoe1  19722  xrsds  19837  uvcvvcl2  20175  uvcff  20178  mamumat1cl  20293  dmatmulcl  20354  scmatscmiddistr  20362  1mavmul  20402  marrepeval  20417  marrepcl  20418  marepveval  20422  marepvcl  20423  mdetrsca2  20458  mdetr0  20459  mdetrlin2  20461  mdetralt2  20463  mdetero  20464  mdetunilem2  20467  mdetunilem5  20470  mdetunilem6  20471  mdetunilem8  20473  mdetunilem9  20474  maducoeval2  20494  maduf  20495  madutpos  20496  madugsum  20497  gsummatr01lem3  20511  marep01ma  20514  smadiadetglem2  20526  monmatcollpw  20632  pmatcollpw3fi1lem1  20639  pmatcollpw3fi1lem2  20640  xkopt  21506  tsmssplit  22002  ssblex  22280  stdbdxmet  22367  stdbdmet  22368  stdbdbl  22369  stdbdmopn  22370  nlmvscnlem1  22537  tgioo  22646  xrsxmet  22659  icccmplem2  22673  ipcnlem1  23090  ivthlem2  23267  ovolicc2lem5  23335  ioombl1lem1  23372  ioombl1lem3  23374  ioombl1lem4  23375  mbfmax  23461  i1fres  23517  itg1climres  23526  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  limcres  23695  dvferm1lem  23792  dvferm2lem  23794  dvlip2  23803  lhop1  23822  dvfsumrlim  23839  mdegaddle  23879  deg1addle2  23907  deg1sublt  23915  ply1divmo  23940  plyaddlem1  24014  plyaddlem  24016  coeaddlem  24050  dgradd2  24069  plydiveu  24098  abelthlem9  24239  logcnlem2  24434  logcnlem3  24435  cxpcn3lem  24533  lgamgulmlem4  24803  lgamgulmlem6  24805  ftalem2  24845  gausslemma2dlem4  25139  chebbnd1lem1  25203  dchrisumlem3  25225  dchrvmasumiflem1  25235  ostth3  25372  axlowdimlem15  25881  dstfrvunirn  30664  circlemeth  30846  indispconn  31342  noprefixmo  31973  knoppndvlem18  32645  itg2addnclem2  33592  itg2addnclem3  33593  ftc1anclem5  33619  irrapxlem4  37706  irrapxlem5  37707  kelac1  37950  areaquad  38119  clsk1indlem4  38659  refsum2cnlem1  39510  rexabslelem  39958  uzublem  39970  ioondisj2  40032  ioondisj1  40033  uzubioo  40112  mullimc  40166  mullimcf  40173  lptioo2  40181  limcleqr  40194  0ellimcdiv  40199  limsupubuzlem  40262  limsupequzmptlem  40278  climxrre  40300  limsup10exlem  40322  limsup10ex  40323  liminf10ex  40324  liminflelimsuplem  40325  icccncfext  40418  cncfiooicclem1  40424  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  stoweid  40598  fourierdlem9  40651  fourierdlem10  40652  fourierdlem37  40679  fourierdlem40  40682  fourierdlem66  40707  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem78  40719  fourierdlem79  40720  fourierdlem95  40736  fourierdlem103  40744  sqwvfoura  40763  fouriersw  40766  etransclem1  40770  etransclem4  40773  etransclem17  40786  etransclem18  40787  etransclem19  40788  etransclem20  40789  etransclem21  40790  etransclem22  40791  etransclem23  40792  etransclem27  40796  etransclem32  40801  etransclem35  40804  etransclem46  40815  ioorrnopnlem  40842  ovnval2  41080  volicorecl  41081  hoiprodcl  41082  ovnf  41098  hsphoif  41111  hsphoival  41114  hoiprodcl3  41115  volicore  41116  hoidmvcl  41117  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoilem1  41136  hoidifhspf  41153  hoidifhspval3  41154  ovolval4lem1  41184  ovolval4lem2  41185  smfmullem1  41319  smfmullem2  41320  smfmullem3  41321  suppmptcfin  42485  linc1  42539  lcoss  42550  el0ldep  42580
  Copyright terms: Public domain W3C validator