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

Theorem ifclda 3889
Description: Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
ifclda.1  |-  ( (
ph  /\  ps )  ->  A  e.  C )
ifclda.2  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
Assertion
Ref Expression
ifclda  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )

Proof of Theorem ifclda
StepHypRef Expression
1 iftrue 3863 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 464 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifclda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
42, 3eqeltrd 2470 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3866 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 464 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifclda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
86, 7eqeltrd 2470 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 789 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    = wceq 1399    e. wcel 1826   ifcif 3857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-if 3858
This theorem is referenced by:  unxpdomlem3  7642  acndom  8345  iunfictbso  8408  dfac12lem2  8437  ttukeylem6  8807  canthp1lem2  8942  xaddf  11344  xmulf  11385  ccatcl  12502  swrdcl  12555  ccatco  12712  lo1bdd2  13349  o1lo1  13362  sadadd2lem2  14102  sadcaddlem  14109  sadadd2lem  14111  sadadd3  14113  iserodd  14361  prmreclem2  14437  prmreclem4  14439  prmreclem6  14441  prmrec  14442  vdwlem6  14506  symgextf  16559  pmtrf  16597  cyggex2  17016  dprdfid  17170  dprdfidOLD  17177  dmdprdsplitlem  17197  dmdprdsplitlemOLD  17198  cygznlem1  18696  cygznlem2a  18697  cygznlem3  18699  cygth  18701  fvmptnn04if  19435  chfacfisf  19440  chfacfisfcpmat  19441  ptpjpre2  20166  ptopn2  20170  ptpjopn  20198  iccpnfcnv  21529  xrhmeo  21531  cmetcaulem  21812  ovolunlem1a  21992  ovolunlem1  21993  ioorf  22067  mbfi1fseqlem3  22209  mbfi1flim  22215  itg2seq  22234  itg2splitlem  22240  itg2split  22241  iblss  22296  itgle  22301  itgeqa  22305  ibladdlem  22311  itgaddlem1  22314  iblabslem  22319  iblabs  22320  iblabsr  22321  iblmulc2  22322  itgmulc2lem1  22323  bddmulibl  22330  itggt0  22333  itgcn  22334  ellimc2  22366  limccnp  22380  limccnp2  22381  dvcobr  22434  lhop1  22500  elplyd  22684  coeeq2  22724  dvply1  22765  aalioulem3  22815  dvtaylp  22850  dvradcnv  22901  psercnlem1  22905  logcnlem2  23111  logcnlem3  23112  logcnlem4  23113  logtayllem  23127  logtayl  23128  cxpcl  23142  recxpcl  23143  leibpilem2  23388  leibpi  23389  rlimcnp2  23413  efrlim  23416  pclogsum  23607  dchrelbasd  23631  lgsfcl2  23694  lgscllem  23695  lgsval2lem  23698  lgsne0  23725  dchrvmasumiflem2  23804  dchrisum0flblem1  23810  pntrlog2bndlem4  23882  pntrlog2bndlem5  23883  pntlemj  23905  padicabv  23932  sgnsval  27871  xrge0iifcnv  28069  xrge0iifhom  28073  pnfneige0  28087  esumpinfval  28221  sigaclfu2  28270  ballotlemsv  28631  ballotlemsdom  28633  signswmnd  28697  signsvvf  28719  signsvfn  28722  igamf  28782  igamcl  28783  mrsubcv  29059  mrsubff  29061  mrsubrn  29062  mrsubccat  29067  itg2addnclem2  30233  itg2gt0cn  30236  ibladdnclem  30237  itgaddnclem1  30239  iblabsnclem  30244  iblabsnc  30245  iblmulc2nc  30246  itgmulc2nclem1  30247  bddiblnc  30251  itggt0cn  30253  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  areacirc  30278  sdrgacs  31318  climsuse  31780  lptioo1  31804  icccncfext  31856  cncfiooicclem1  31862  iblsplit  31931  dirkerval2  32042  dirkerre  32043  fourierdlem9  32064  fourierdlem17  32072  fourierdlem43  32098  etransclem3  32186  etransclem7  32190  etransclem10  32193  etransclem21  32204  lincext1  33255  cdleme27cl  36505
  Copyright terms: Public domain W3C validator