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

Theorem ifclda 3958
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 3932 . . . 4  |-  ( ps 
->  if ( ps ,  A ,  B )  =  A )
21adantl 466 . . 3  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  =  A )
3 ifclda.1 . . 3  |-  ( (
ph  /\  ps )  ->  A  e.  C )
42, 3eqeltrd 2531 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3935 . . . 4  |-  ( -. 
ps  ->  if ( ps ,  A ,  B
)  =  B )
65adantl 466 . . 3  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  =  B )
7 ifclda.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  B  e.  C )
86, 7eqeltrd 2531 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 791 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804   ifcif 3926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-if 3927
This theorem is referenced by:  unxpdomlem3  7728  acndom  8435  iunfictbso  8498  dfac12lem2  8527  ttukeylem6  8897  canthp1lem2  9034  xaddf  11434  xmulf  11475  ccatcl  12575  swrdcl  12628  ccatco  12783  lo1bdd2  13329  o1lo1  13342  sadadd2lem2  14082  sadcaddlem  14089  sadadd2lem  14091  sadadd3  14093  iserodd  14341  prmreclem2  14417  prmreclem4  14419  prmreclem6  14421  prmrec  14422  vdwlem6  14486  symgextf  16421  pmtrf  16459  cyggex2  16878  dprdfid  17036  dprdfidOLD  17043  dmdprdsplitlem  17063  dmdprdsplitlemOLD  17064  cygznlem1  18583  cygznlem2a  18584  cygznlem3  18586  cygth  18588  fvmptnn04if  19328  chfacfisf  19333  chfacfisfcpmat  19334  ptpjpre2  20059  ptopn2  20063  ptpjopn  20091  iccpnfcnv  21422  xrhmeo  21424  cmetcaulem  21705  ovolunlem1a  21885  ovolunlem1  21886  ioorf  21960  mbfi1fseqlem3  22102  mbfi1flim  22108  itg2seq  22127  itg2splitlem  22133  itg2split  22134  iblss  22189  itgle  22194  itgeqa  22198  ibladdlem  22204  itgaddlem1  22207  iblabslem  22212  iblabs  22213  iblabsr  22214  iblmulc2  22215  itgmulc2lem1  22216  bddmulibl  22223  itggt0  22226  itgcn  22227  ellimc2  22259  limccnp  22273  limccnp2  22274  dvcobr  22327  lhop1  22393  elplyd  22577  coeeq2  22617  dvply1  22658  aalioulem3  22708  dvtaylp  22743  dvradcnv  22794  psercnlem1  22798  logcnlem2  23002  logcnlem3  23003  logcnlem4  23004  logtayllem  23018  logtayl  23019  cxpcl  23033  recxpcl  23034  leibpilem2  23250  leibpi  23251  rlimcnp2  23274  efrlim  23277  pclogsum  23468  dchrelbasd  23492  lgsfcl2  23555  lgscllem  23556  lgsval2lem  23559  lgsne0  23586  dchrvmasumiflem2  23665  dchrisum0flblem1  23671  pntrlog2bndlem4  23743  pntrlog2bndlem5  23744  pntlemj  23766  padicabv  23793  sgnsval  27696  xrge0iifcnv  27893  xrge0iifhom  27897  pnfneige0  27911  esumpinfval  28057  sigaclfu2  28099  ballotlemsv  28426  ballotlemsdom  28428  signswmnd  28492  signsvvf  28514  signsvfn  28517  igamf  28571  igamcl  28572  mrsubcv  28848  mrsubff  28850  mrsubrn  28851  mrsubccat  28856  itg2addnclem2  30043  itg2gt0cn  30046  ibladdnclem  30047  itgaddnclem1  30049  iblabsnclem  30054  iblabsnc  30055  iblmulc2nc  30056  itgmulc2nclem1  30057  bddiblnc  30061  itggt0cn  30063  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  areacirc  30088  sdrgacs  31126  climsuse  31568  lptioo1  31592  icccncfext  31644  cncfiooicclem1  31650  iblsplit  31719  dirkerval2  31830  dirkerre  31831  fourierdlem9  31852  fourierdlem17  31860  fourierdlem43  31886  lincext1  32925  cdleme27cl  35967
  Copyright terms: Public domain W3C validator