Theorem ifcld 3935

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 3934	. 2 |- ( ( A e. C /\ B e. C ) -> if ( ps , A , B ) e. C )
4	1, 2, 3	syl2anc 671	1 |- ( ph -> if ( ps , A , B ) e. C )

Syntax hints:   -> wi 4   e. wcel 1897   ifcif 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-if 3893

This theorem is referenced by:  soltmin  5254  pw2f1olem  7701  unxpdomlem3  7803  wemaplem2  8087  cantnfp1lem1  8208  cantnfp1lem2  8209  cantnfp1lem3  8210  cantnflem1d  8218  cantnflem1  8219  relexpsucnnr  13136  rexuzre  13463  rexico  13464  limsupgre  13590  limsupgreOLD  13591  rlim3  13610  o1lo1  13649  rlimclim1  13657  lo1resb  13676  o1resb  13678  o1of2  13724  o1rlimmul  13730  lo1le  13763  ruclem1  14331  ruclem10  14339  bitsfzo  14457  ramub1lem2  15033  ramcl  15035  prmocl  15040  prmop1  15044  prmdvdsprmo  15048  prmolefac  15052  prmodvdslcmf  15053  prmormapnnOLD  15062  prmdvdsprmorOLD  15063  prmorlefacOLD  15066  prmordvdslcmfOLD  15067  prmordvdslcmsOLDOLD  15069  prmgapprmo  15081  wunress  15237  opifismgm  16549  frgpuptf  17468  gsumzsplit  17608  gsummpt1n0  17645  snifpsrbag  18638  psr1cl  18674  subrgpsr  18691  mvrf  18696  mplmon  18735  mplmonmul  18736  mplcoe1  18737  evlslem3  18785  evlslem1  18786  coe1tmfv2  18916  gsummoncoe1  18946  xrsds  19059  uvcvvcl2  19394  uvcff  19397  mamumat1cl  19512  dmatmulcl  19573  scmatscmiddistr  19581  1mavmul  19621  marrepeval  19636  marrepcl  19637  marepveval  19641  marepvcl  19642  mdetrsca2  19677  mdetr0  19678  mdetrlin2  19680  mdetralt2  19682  mdetero  19683  mdetunilem2  19686  mdetunilem5  19689  mdetunilem6  19690  mdetunilem8  19692  mdetunilem9  19693  maducoeval2  19713  maduf  19714  madutpos  19715  madugsum  19716  gsummatr01lem3  19730  marep01ma  19733  smadiadetglem2  19745  monmatcollpw  19851  pmatcollpw3fi1lem1  19858  pmatcollpw3fi1lem2  19859  xkopt  20718  tsmssplit  21214  ssblex  21491  stdbdxmet  21578  stdbdmet  21579  stdbdbl  21580  stdbdmopn  21581  nlmvscnlem1  21737  tgioo  21862  xrsxmet  21875  icccmplem2  21889  ipcnlem1  22264  ivthlem2  22451  ovolicc2lem5  22523  ioombl1lem1  22559  ioombl1lem3  22561  ioombl1lem4  22562  mbfmax  22653  i1fres  22711  itg1climres  22720  mbfi1fseqlem3  22723  mbfi1fseqlem4  22724  mbfi1fseqlem5  22725  limcres  22889  dvferm1lem  22984  dvferm2lem  22986  dvlip2  22995  lhop1  23014  dvfsumrlim  23031  mdegaddle  23071  deg1addle2  23099  deg1sublt  23107  ply1divmo  23134  plyaddlem1  23215  plyaddlem  23217  coeaddlem  23251  dgradd2  23270  plydiveu  23299  abelthlem9  23443  logcnlem2  23636  logcnlem3  23637  cxpcn3lem  23735  lgamgulmlem4  24005  lgamgulmlem6  24007  ftalem2  24046  chebbnd1lem1  24355  dchrisumlem3  24377  dchrvmasumiflem1  24387  ostth3  24524  axlowdimlem15  25034  dstfrvunirn  29355  indispcon  30005  itg2addnclem2  32038  itg2addnclem3  32039  ftc1anclem5  32065  irrapxlem4  35713  irrapxlem5  35714  kelac1  35965  areaquad  36145  refsum2cnlem1  37397  ioondisj2  37626  ioondisj1  37627  mullimc  37733  mullimcf  37740  lptioo2  37748  limcleqr  37762  0ellimcdiv  37767  icccncfext  37802  cncfiooicclem1  37808  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  stoweid  37962  fourierdlem9  38015  fourierdlem10  38016  fourierdlem37  38044  fourierdlem40  38047  fourierdlem66  38073  fourierdlem73  38080  fourierdlem74  38081  fourierdlem75  38082  fourierdlem78  38085  fourierdlem79  38086  fourierdlem95  38102  fourierdlem103  38110  sqwvfoura  38129  fouriersw  38132  etransclem1  38137  etransclem4  38140  etransclem17  38153  etransclem18  38154  etransclem19  38155  etransclem20  38156  etransclem21  38157  etransclem22  38158  etransclem23  38159  etransclem27  38163  etransclem32  38168  etransclem35  38171  etransclem46  38182  ovnval2  38404  volicorecl  38405  hoiprodcl  38406  ovnf  38422  hsphoif  38435  hsphoival  38438  hoiprodcl3  38439  volicore  38440  hoidmvcl  38441  hsphoidmvle2  38444  hsphoidmvle  38445  hoidmv1lelem1  38450  hoidmv1lelem2  38451  hoidmv1lelem3  38452  hoidmvlelem2  38455  hoidmvlelem3  38456  ovnhoilem1  38460  hoidifhspf  38477  hoidifhspval3  38478  suppmptcfin  40436  linc1  40490  lcoss  40501  el0ldep  40531