Theorem ifcld 3984

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

Proof of Theorem ifcld

Step	Hyp	Ref	Expression
1		ifcld.a	. 2
2		ifcld.b	. 2
3		ifcl 3983	. 2
4	1, 2, 3	syl2anc 661	1

Syntax hints:  ->wi 4  e.wcel 1818  ifcif 3941

This theorem is referenced by:  soltmin  5411  pw2f1olem  7641  unxpdomlem3  7746  wemaplem2  7993  cantnfp1lem1  8118  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnflem1d  8128  cantnflem1  8129  rexuzre  13185  rexico  13186  limsupgre  13304  rlim3  13321  o1lo1  13360  rlimclim1  13368  lo1resb  13387  o1resb  13389  o1of2  13435  o1rlimmul  13441  lo1le  13474  ruclem1  13964  ruclem10  13972  bitsfzo  14085  ramub1lem2  14545  ramcl  14547  wunress  14696  opifismgm  15885  frgpuptf  16788  gsumzsplit  16944  gsummpt1n0  16992  snifpsrbag  18015  psr1cl  18055  subrgpsr  18074  mvrf  18080  mplmon  18125  mplmonmul  18126  mplcoe1  18127  evlslem3  18183  evlslem1  18184  coe1tmfv2  18316  gsummoncoe1  18346  xrsds  18461  uvcvvcl2  18819  uvcff  18822  mamumat1cl  18941  dmatmulcl  19002  scmatscmiddistr  19010  1mavmul  19050  marrepeval  19065  marrepcl  19066  marepveval  19070  marepvcl  19071  mdetrsca2  19106  mdetr0  19107  mdetrlin2  19109  mdetralt2  19111  mdetero  19112  mdetunilem2  19115  mdetunilem5  19118  mdetunilem6  19119  mdetunilem8  19121  mdetunilem9  19122  maducoeval2  19142  maduf  19143  madutpos  19144  madugsum  19145  gsummatr01lem3  19159  marep01ma  19162  smadiadetglem2  19174  monmatcollpw  19280  pmatcollpw3fi1lem1  19287  pmatcollpw3fi1lem2  19288  xkopt  20156  tsmssplit  20654  ssblex  20931  stdbdxmet  21018  stdbdmet  21019  stdbdbl  21020  stdbdmopn  21021  nlmvscnlem1  21195  tgioo  21301  xrsxmet  21314  icccmplem2  21328  ipcnlem1  21685  ivthlem2  21864  ovolicc2lem5  21932  ioombl1lem1  21968  ioombl1lem3  21970  ioombl1lem4  21971  mbfmax  22056  i1fres  22112  itg1climres  22121  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  limcres  22290  dvferm1lem  22385  dvferm2lem  22387  dvlip2  22396  lhop1  22415  dvfsumrlim  22432  mdegaddle  22474  deg1addle2  22503  deg1sublt  22511  ply1divmo  22536  plyaddlem1  22610  plyaddlem  22612  coeaddlem  22646  dgradd2  22665  plydiveu  22694  abelthlem9  22835  logcnlem2  23024  logcnlem3  23025  cxpcn3lem  23121  ftalem2  23347  chebbnd1lem1  23654  dchrisumlem3  23676  dchrvmasumiflem1  23686  ostth3  23823  axlowdimlem15  24259  dstfrvunirn  28413  lgamgulmlem4  28574  lgamgulmlem6  28576  indispcon  28679  itg2addnclem2  30067  itg2addnclem3  30068  ftc1anclem5  30094  irrapxlem4  30761  irrapxlem5  30762  kelac1  31009  areaquad  31184  refsum2cnlem1  31412  ioondisj2  31525  ioondisj1  31526  mullimc  31622  mullimcf  31629  lptioo2  31637  limcleqr  31650  0ellimcdiv  31655  icccncfext  31690  cncfiooicclem1  31696  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweid  31845  fourierdlem9  31898  fourierdlem10  31899  fourierdlem37  31926  fourierdlem40  31929  fourierdlem66  31955  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem79  31968  fourierdlem95  31984  fourierdlem103  31992  sqwvfoura  32011  fouriersw  32014  etransclem1  32018  etransclem4  32021  etransclem17  32034  etransclem18  32035  etransclem19  32036  etransclem20  32037  etransclem21  32038  etransclem22  32039  etransclem23  32040  etransclem27  32044  etransclem32  32049  etransclem35  32052  etransclem46  32063  suppmptcfin  32972  linc1  33026  lcoss  33037  el0ldep  33067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942