MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifcld Structured version   Unicode version

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
StepHypRef 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 )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator