Theorem ifcld 3892

Description: Membership (closure) of a conditional operator, deduction form. (Contributed by SO, 16-Jul-2018.)

Hypotheses

Ref	Expression
ifcld.a	|- ( ph -> A e. C )
ifcld.b	|- ( ph -> B e. C )

Assertion

Ref	Expression
ifcld	|- ( ph -> if ( ps , A , B ) e. C )

Proof of Theorem ifcld

Step	Hyp	Ref	Expression
1		ifcld.a	. 2 |- ( ph -> A e. C )
2		ifcld.b	. 2 |- ( ph -> B e. C )
3		ifcl 3891	. 2 |- ( ( A e. C /\ B e. C ) -> if ( ps , A , B ) e. C )
4	1, 2, 3	syl2anc 665	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -> wi 4   e. wcel 1872   ifcif 3849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-if 3850

This theorem is referenced by:  soltmin  5193  pw2f1olem  7624  unxpdomlem3  7726  wemaplem2  8010  cantnfp1lem1  8130  cantnfp1lem2  8131  cantnfp1lem3  8132  cantnflem1d  8140  cantnflem1  8141  relexpsucnnr  13027  rexuzre  13354  rexico  13355  limsupgre  13480  limsupgreOLD  13481  rlim3  13500  o1lo1  13539  rlimclim1  13547  lo1resb  13566  o1resb  13568  o1of2  13614  o1rlimmul  13620  lo1le  13653  ruclem1  14221  ruclem10  14229  bitsfzo  14347  ramub1lem2  14923  ramcl  14925  prmocl  14930  prmop1  14934  prmdvdsprmo  14938  prmolefac  14942  prmodvdslcmf  14943  prmormapnnOLD  14952  prmdvdsprmorOLD  14953  prmorlefacOLD  14956  prmordvdslcmfOLD  14957  prmordvdslcmsOLDOLD  14959  prmgapprmo  14971  wunress  15127  opifismgm  16439  frgpuptf  17358  gsumzsplit  17498  gsummpt1n0  17535  snifpsrbag  18528  psr1cl  18564  subrgpsr  18581  mvrf  18586  mplmon  18625  mplmonmul  18626  mplcoe1  18627  evlslem3  18675  evlslem1  18676  coe1tmfv2  18806  gsummoncoe1  18836  xrsds  18949  uvcvvcl2  19283  uvcff  19286  mamumat1cl  19401  dmatmulcl  19462  scmatscmiddistr  19470  1mavmul  19510  marrepeval  19525  marrepcl  19526  marepveval  19530  marepvcl  19531  mdetrsca2  19566  mdetr0  19567  mdetrlin2  19569  mdetralt2  19571  mdetero  19572  mdetunilem2  19575  mdetunilem5  19578  mdetunilem6  19579  mdetunilem8  19581  mdetunilem9  19582  maducoeval2  19602  maduf  19603  madutpos  19604  madugsum  19605  gsummatr01lem3  19619  marep01ma  19622  smadiadetglem2  19634  monmatcollpw  19740  pmatcollpw3fi1lem1  19747  pmatcollpw3fi1lem2  19748  xkopt  20607  tsmssplit  21103  ssblex  21380  stdbdxmet  21467  stdbdmet  21468  stdbdbl  21469  stdbdmopn  21470  nlmvscnlem1  21626  tgioo  21751  xrsxmet  21764  icccmplem2  21778  ipcnlem1  22153  ivthlem2  22340  ovolicc2lem5  22412  ioombl1lem1  22448  ioombl1lem3  22450  ioombl1lem4  22451  mbfmax  22542  i1fres  22600  itg1climres  22609  mbfi1fseqlem3  22612  mbfi1fseqlem4  22613  mbfi1fseqlem5  22614  limcres  22778  dvferm1lem  22873  dvferm2lem  22875  dvlip2  22884  lhop1  22903  dvfsumrlim  22920  mdegaddle  22960  deg1addle2  22988  deg1sublt  22996  ply1divmo  23023  plyaddlem1  23104  plyaddlem  23106  coeaddlem  23140  dgradd2  23159  plydiveu  23188  abelthlem9  23332  logcnlem2  23525  logcnlem3  23526  cxpcn3lem  23624  lgamgulmlem4  23894  lgamgulmlem6  23896  ftalem2  23935  chebbnd1lem1  24244  dchrisumlem3  24266  dchrvmasumiflem1  24276  ostth3  24413  axlowdimlem15  24923  dstfrvunirn  29254  indispcon  29904  itg2addnclem2  31901  itg2addnclem3  31902  ftc1anclem5  31928  irrapxlem4  35582  irrapxlem5  35583  kelac1  35834  areaquad  36014  refsum2cnlem1  37274  ioondisj2  37481  ioondisj1  37482  mullimc  37579  mullimcf  37586  lptioo2  37594  limcleqr  37608  0ellimcdiv  37613  icccncfext  37648  cncfiooicclem1  37654  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  stoweid  37808  fourierdlem9  37861  fourierdlem10  37862  fourierdlem37  37890  fourierdlem40  37893  fourierdlem66  37919  fourierdlem73  37926  fourierdlem74  37927  fourierdlem75  37928  fourierdlem78  37931  fourierdlem79  37932  fourierdlem95  37948  fourierdlem103  37956  sqwvfoura  37975  fouriersw  37978  etransclem1  37983  etransclem4  37986  etransclem17  37999  etransclem18  38000  etransclem19  38001  etransclem20  38002  etransclem21  38003  etransclem22  38004  etransclem23  38005  etransclem27  38009  etransclem32  38014  etransclem35  38017  etransclem46  38028  ovnval2  38214  volicorecl  38215  hoiprodcl  38216  ovnf  38232  hsphoif  38245  hsphoival  38248  hoiprodcl3  38249  volicore  38250  hoidmvcl  38251  hsphoidmvle2  38254  hsphoidmvle  38255  hoidmv1lelem1  38260  hoidmv1lelem2  38261  hoidmv1lelem3  38262  hoidmvlelem2  38265  hoidmvlelem3  38266  ovnhoilem1  38270  suppmptcfin  39757  linc1  39811  lcoss  39822  el0ldep  39852