Theorem ifcld 3982

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

Syntax hints:   -> wi 4   e. wcel 1767   ifcif 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940

This theorem is referenced by:  cantnfp1lem1  8093  cantnfp1lem2  8094  cantnfp1lem3  8095  cantnflem1d  8103  cantnflem1  8104  gsumzsplit  16735  gsummpt1n0  16783  snifpsrbag  17786  mplmon  17896  mplmonmul  17897  mplcoe1  17898  evlslem3  17954  evlslem1  17955  gsummoncoe1  18117  uvcff  18589  dmatmulcl  18769  scmatscmiddistr  18777  1mavmul  18817  marrepeval  18832  marrepcl  18833  marepveval  18837  marepvcl  18838  mdetrsca2  18873  mdetr0  18874  mdetrlin2  18876  mdetralt2  18878  mdetero  18879  mdetunilem2  18882  mdetunilem5  18885  mdetunilem6  18886  mdetunilem8  18888  mdetunilem9  18889  maducoeval2  18909  madutpos  18911  madugsum  18912  gsummatr01lem3  18926  marep01ma  18929  smadiadetglem2  18941  monmatcollpw  19047  pmatcollpw3fi1lem1  19054  pmatcollpw3fi1lem2  19055  tsmssplit  20389  areaquad  30789  limcleqr  31186  addlimc  31190  0ellimcdiv  31191  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweid  31363  fourierdlem9  31416  fourierdlem10  31417  fourierdlem37  31444  fourierdlem40  31447  fourierdlem66  31473  fourierdlem73  31480  fourierdlem74  31481  fourierdlem75  31482  fourierdlem78  31485  fourierdlem79  31486  fourierdlem95  31502  fourierdlem103  31510  sqwvfoura  31529  fouriersw  31532  suppmptcfin  32045  linc1  32099  lcoss  32110  el0ldep  32140