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

Theorem ifclda 3915
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 3889 . . . 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 2531 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3892 . . . 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 2531 . 2  |-  ( (
ph  /\  -.  ps )  ->  if ( ps ,  A ,  B )  e.  C )
94, 8pm2.61dan 801 1  |-  ( ph  ->  if ( ps ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 371    = wceq 1446    e. wcel 1889   ifcif 3883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3884
This theorem is referenced by:  unxpdomlem3  7783  acndom  8487  iunfictbso  8550  dfac12lem2  8579  ttukeylem6  8949  canthp1lem2  9083  xaddf  11524  xmulf  11565  ccatcl  12727  swrdcl  12782  ccatco  12939  lo1bdd2  13600  o1lo1  13613  sadadd2lem2  14436  sadcaddlem  14443  sadadd2lem  14445  sadadd3  14447  lcmfval  14603  lcmfvalOLD  14607  iserodd  14797  prmreclem2  14873  prmreclem4  14875  prmreclem6  14877  prmrec  14878  vdwlem6  14948  symgextf  17070  pmtrf  17108  cyggex2  17543  dprdfid  17662  dmdprdsplitlem  17682  cygznlem1  19149  cygznlem2a  19150  cygznlem3  19152  cygth  19154  fvmptnn04if  19885  chfacfisf  19890  chfacfisfcpmat  19891  ptpjpre2  20607  ptopn2  20611  ptpjopn  20639  iccpnfcnv  21984  xrhmeo  21986  cmetcaulem  22270  ovolunlem1a  22461  ovolunlem1  22462  ioorf  22537  ioorfOLD  22542  mbfi1fseqlem3  22687  mbfi1flim  22693  itg2seq  22712  itg2splitlem  22718  itg2split  22719  iblss  22774  itgle  22779  itgeqa  22783  ibladdlem  22789  itgaddlem1  22792  iblabslem  22797  iblabs  22798  iblabsr  22799  iblmulc2  22800  itgmulc2lem1  22801  bddmulibl  22808  itggt0  22811  itgcn  22812  ellimc2  22844  limccnp  22858  limccnp2  22859  dvcobr  22912  lhop1  22978  elplyd  23168  coeeq2  23208  dvply1  23249  aalioulem3  23302  dvtaylp  23337  dvradcnv  23388  psercnlem1  23392  logcnlem2  23600  logcnlem3  23601  logcnlem4  23602  logtayllem  23616  logtayl  23617  cxpcl  23631  recxpcl  23632  leibpilem2  23879  leibpi  23880  rlimcnp2  23904  efrlim  23907  igamf  23988  igamcl  23989  pclogsum  24155  dchrelbasd  24179  lgsfcl2  24242  lgscllem  24243  lgsval2lem  24246  lgsne0  24273  dchrvmasumiflem2  24352  dchrisum0flblem1  24358  pntrlog2bndlem4  24430  pntrlog2bndlem5  24431  pntlemj  24453  padicabv  24480  sgnsval  28503  xrge0iifcnv  28751  xrge0iifhom  28755  pnfneige0  28769  esumpinfval  28906  sigaclfu2  28955  ballotlemsv  29354  ballotlemsdom  29356  ballotlemsvOLD  29392  ballotlemsdomOLD  29394  signswmnd  29458  signsvvf  29480  signsvfn  29483  mrsubcv  30160  mrsubff  30162  mrsubrn  30163  mrsubccat  30168  ptrecube  31952  poimirlem24  31976  itg2addnclem2  32006  itg2gt0cn  32009  ibladdnclem  32010  itgaddnclem1  32012  iblabsnclem  32017  iblabsnc  32018  iblmulc2nc  32019  itgmulc2nclem1  32020  bddiblnc  32024  itggt0cn  32026  ftc1anclem5  32033  ftc1anclem6  32034  ftc1anclem7  32035  ftc1anclem8  32036  ftc1anc  32037  areacirc  32049  cdleme27cl  33945  sdrgacs  36079  climsuse  37697  lptioo1  37722  icccncfext  37775  cncfiooicclem1  37781  iblsplit  37853  dirkerval2  37966  dirkerre  37967  fourierdlem9  37988  fourierdlem17  37996  fourierdlem43  38024  etransclem3  38112  etransclem7  38116  etransclem10  38119  etransclem21  38130  lincext1  40351
  Copyright terms: Public domain W3C validator