Theorem ifcld 3932

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 3931	. 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 1758   ifcif 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-if 3892

This theorem is referenced by:  cantnfp1lem1  7989  cantnfp1lem2  7990  cantnfp1lem3  7991  cantnflem1d  7999  cantnflem1  8000  gsumzsplit  16524  gsummpt1n0  16563  snifpsrbag  17541  mplmon  17651  mplmonmul  17652  mplcoe1  17653  evlslem3  17709  evlslem1  17710  uvcff  18327  1mavmul  18472  marrepeval  18487  marrepcl  18488  marepveval  18492  marepvcl  18493  mdetrsca2  18528  mdetr0  18529  mdetrlin2  18531  mdetralt2  18533  mdetero  18534  mdetunilem2  18537  mdetunilem5  18540  mdetunilem6  18541  mdetunilem8  18543  mdetunilem9  18544  maducoeval2  18564  madutpos  18566  madugsum  18567  gsummatr01lem3  18581  marep01ma  18584  smadiadetglem2  18596  tsmssplit  19844  areaquad  29732  stoweid  29998  suppmptcfin  30933  gsummoncoe1  30987  dmatmulcl  31035  scmatmulcl  31042  linc1  31068  lcoss  31079  el0ldep  31109  monmatcollpw  31238  pmatcollpw4fi1lem1  31244  pmatcollpw4fi1lem2  31245