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

Theorem ifclda 3942
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 3916 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 468 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifclda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
42, 3eqeltrd 2511 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3919 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 468 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifclda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
86, 7eqeltrd 2511 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 799 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 371    = wceq 1438    e. wcel 1869   ifcif 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-if 3911
This theorem is referenced by:  unxpdomlem3  7782  acndom  8484  iunfictbso  8547  dfac12lem2  8576  ttukeylem6  8946  canthp1lem2  9080  xaddf  11519  xmulf  11560  ccatcl  12718  swrdcl  12771  ccatco  12928  lo1bdd2  13581  o1lo1  13594  sadadd2lem2  14417  sadcaddlem  14424  sadadd2lem  14426  sadadd3  14428  lcmfval  14584  lcmfvalOLD  14588  iserodd  14778  prmreclem2  14854  prmreclem4  14856  prmreclem6  14858  prmrec  14859  vdwlem6  14929  symgextf  17051  pmtrf  17089  cyggex2  17524  dprdfid  17643  dmdprdsplitlem  17663  cygznlem1  19129  cygznlem2a  19130  cygznlem3  19132  cygth  19134  fvmptnn04if  19865  chfacfisf  19870  chfacfisfcpmat  19871  ptpjpre2  20587  ptopn2  20591  ptpjopn  20619  iccpnfcnv  21964  xrhmeo  21966  cmetcaulem  22250  ovolunlem1a  22441  ovolunlem1  22442  ioorf  22517  ioorfOLD  22522  mbfi1fseqlem3  22667  mbfi1flim  22673  itg2seq  22692  itg2splitlem  22698  itg2split  22699  iblss  22754  itgle  22759  itgeqa  22763  ibladdlem  22769  itgaddlem1  22772  iblabslem  22777  iblabs  22778  iblabsr  22779  iblmulc2  22780  itgmulc2lem1  22781  bddmulibl  22788  itggt0  22791  itgcn  22792  ellimc2  22824  limccnp  22838  limccnp2  22839  dvcobr  22892  lhop1  22958  elplyd  23148  coeeq2  23188  dvply1  23229  aalioulem3  23282  dvtaylp  23317  dvradcnv  23368  psercnlem1  23372  logcnlem2  23580  logcnlem3  23581  logcnlem4  23582  logtayllem  23596  logtayl  23597  cxpcl  23611  recxpcl  23612  leibpilem2  23859  leibpi  23860  rlimcnp2  23884  efrlim  23887  igamf  23968  igamcl  23969  pclogsum  24135  dchrelbasd  24159  lgsfcl2  24222  lgscllem  24223  lgsval2lem  24226  lgsne0  24253  dchrvmasumiflem2  24332  dchrisum0flblem1  24338  pntrlog2bndlem4  24410  pntrlog2bndlem5  24411  pntlemj  24433  padicabv  24460  sgnsval  28492  xrge0iifcnv  28741  xrge0iifhom  28745  pnfneige0  28759  esumpinfval  28896  sigaclfu2  28945  ballotlemsv  29344  ballotlemsdom  29346  ballotlemsvOLD  29382  ballotlemsdomOLD  29384  signswmnd  29448  signsvvf  29470  signsvfn  29473  mrsubcv  30150  mrsubff  30152  mrsubrn  30153  mrsubccat  30158  ptrecube  31898  poimirlem24  31922  itg2addnclem2  31952  itg2gt0cn  31955  ibladdnclem  31956  itgaddnclem1  31958  iblabsnclem  31963  iblabsnc  31964  iblmulc2nc  31965  itgmulc2nclem1  31966  bddiblnc  31970  itggt0cn  31972  ftc1anclem5  31979  ftc1anclem6  31980  ftc1anclem7  31981  ftc1anclem8  31982  ftc1anc  31983  areacirc  31995  cdleme27cl  33896  sdrgacs  36031  climsuse  37551  lptioo1  37576  icccncfext  37629  cncfiooicclem1  37635  iblsplit  37707  dirkerval2  37820  dirkerre  37821  fourierdlem9  37842  fourierdlem17  37850  fourierdlem43  37878  etransclem3  37966  etransclem7  37970  etransclem10  37973  etransclem21  37984  lincext1  39591
  Copyright terms: Public domain W3C validator