Theorem ifcld 3972

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

Syntax hints:   -> wi 4   e. wcel 1823   ifcif 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3930

This theorem is referenced by:  soltmin  5391  pw2f1olem  7614  unxpdomlem3  7719  wemaplem2  7964  cantnfp1lem1  8088  cantnfp1lem2  8089  cantnfp1lem3  8090  cantnflem1d  8098  cantnflem1  8099  relexpsucnnr  12942  rexuzre  13267  rexico  13268  limsupgre  13386  rlim3  13403  o1lo1  13442  rlimclim1  13450  lo1resb  13469  o1resb  13471  o1of2  13517  o1rlimmul  13523  lo1le  13556  ruclem1  14048  ruclem10  14056  bitsfzo  14169  ramub1lem2  14629  ramcl  14631  wunress  14783  opifismgm  16084  frgpuptf  16987  gsumzsplit  17143  gsummpt1n0  17188  snifpsrbag  18210  psr1cl  18250  subrgpsr  18269  mvrf  18275  mplmon  18320  mplmonmul  18321  mplcoe1  18322  evlslem3  18378  evlslem1  18379  coe1tmfv2  18511  gsummoncoe1  18541  xrsds  18656  uvcvvcl2  18990  uvcff  18993  mamumat1cl  19108  dmatmulcl  19169  scmatscmiddistr  19177  1mavmul  19217  marrepeval  19232  marrepcl  19233  marepveval  19237  marepvcl  19238  mdetrsca2  19273  mdetr0  19274  mdetrlin2  19276  mdetralt2  19278  mdetero  19279  mdetunilem2  19282  mdetunilem5  19285  mdetunilem6  19286  mdetunilem8  19288  mdetunilem9  19289  maducoeval2  19309  maduf  19310  madutpos  19311  madugsum  19312  gsummatr01lem3  19326  marep01ma  19329  smadiadetglem2  19341  monmatcollpw  19447  pmatcollpw3fi1lem1  19454  pmatcollpw3fi1lem2  19455  xkopt  20322  tsmssplit  20820  ssblex  21097  stdbdxmet  21184  stdbdmet  21185  stdbdbl  21186  stdbdmopn  21187  nlmvscnlem1  21361  tgioo  21467  xrsxmet  21480  icccmplem2  21494  ipcnlem1  21851  ivthlem2  22030  ovolicc2lem5  22098  ioombl1lem1  22134  ioombl1lem3  22136  ioombl1lem4  22137  mbfmax  22222  i1fres  22278  itg1climres  22287  mbfi1fseqlem3  22290  mbfi1fseqlem4  22291  mbfi1fseqlem5  22292  limcres  22456  dvferm1lem  22551  dvferm2lem  22553  dvlip2  22562  lhop1  22581  dvfsumrlim  22598  mdegaddle  22640  deg1addle2  22669  deg1sublt  22677  ply1divmo  22702  plyaddlem1  22776  plyaddlem  22778  coeaddlem  22812  dgradd2  22831  plydiveu  22860  abelthlem9  23001  logcnlem2  23192  logcnlem3  23193  cxpcn3lem  23289  ftalem2  23545  chebbnd1lem1  23852  dchrisumlem3  23874  dchrvmasumiflem1  23884  ostth3  24021  axlowdimlem15  24461  dstfrvunirn  28677  lgamgulmlem4  28838  lgamgulmlem6  28840  indispcon  28943  itg2addnclem2  30307  itg2addnclem3  30308  ftc1anclem5  30334  irrapxlem4  31000  irrapxlem5  31001  kelac1  31248  areaquad  31425  refsum2cnlem1  31652  ioondisj2  31764  ioondisj1  31765  mullimc  31861  mullimcf  31868  lptioo2  31876  limcleqr  31889  0ellimcdiv  31894  icccncfext  31929  cncfiooicclem1  31935  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  stoweid  32084  fourierdlem9  32137  fourierdlem10  32138  fourierdlem37  32165  fourierdlem40  32168  fourierdlem66  32194  fourierdlem73  32201  fourierdlem74  32202  fourierdlem75  32203  fourierdlem78  32206  fourierdlem79  32207  fourierdlem95  32223  fourierdlem103  32231  sqwvfoura  32250  fouriersw  32253  etransclem1  32257  etransclem4  32260  etransclem17  32273  etransclem18  32274  etransclem19  32275  etransclem20  32276  etransclem21  32277  etransclem22  32278  etransclem23  32279  etransclem27  32283  etransclem32  32288  etransclem35  32291  etransclem46  32302  suppmptcfin  33226  linc1  33280  lcoss  33291  el0ldep  33321