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

Theorem ifclda 3971
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 3945 . . . 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 2555 . 2  |-  ( (
ph  /\  ps )  ->  if ( ps ,  A ,  B )  e.  C )
5 iffalse 3948 . . . 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 2555 . 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 369    = wceq 1379    e. wcel 1767   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940
This theorem is referenced by:  unxpdomlem3  7726  acndom  8431  iunfictbso  8494  dfac12lem2  8523  ttukeylem6  8893  canthp1lem2  9030  xaddf  11422  xmulf  11463  ccatcl  12557  swrdcl  12608  ccatco  12763  lo1bdd2  13309  o1lo1  13322  sadadd2lem2  13958  sadcaddlem  13965  sadadd2lem  13967  sadadd3  13969  iserodd  14217  prmreclem2  14293  prmreclem4  14295  prmreclem6  14297  prmrec  14298  vdwlem6  14362  symgextf  16244  pmtrf  16283  cyggex2  16699  dprdfid  16856  dprdfidOLD  16863  dmdprdsplitlem  16883  dmdprdsplitlemOLD  16884  cygznlem1  18388  cygznlem2a  18389  cygznlem3  18391  cygth  18393  fvmptnn04if  19133  chfacfisf  19138  chfacfisfcpmat  19139  ptpjpre2  19832  ptopn2  19836  ptpjopn  19864  iccpnfcnv  21195  xrhmeo  21197  cmetcaulem  21478  ovolunlem1a  21658  ovolunlem1  21659  ioorf  21733  mbfi1fseqlem3  21875  mbfi1flim  21881  itg2seq  21900  itg2splitlem  21906  itg2split  21907  iblss  21962  itgle  21967  itgeqa  21971  ibladdlem  21977  itgaddlem1  21980  iblabslem  21985  iblabs  21986  iblabsr  21987  iblmulc2  21988  itgmulc2lem1  21989  bddmulibl  21996  itggt0  21999  itgcn  22000  ellimc2  22032  limccnp  22046  limccnp2  22047  dvcobr  22100  lhop1  22166  elplyd  22350  coeeq2  22390  dvply1  22430  aalioulem3  22480  dvtaylp  22515  dvradcnv  22566  psercnlem1  22570  logcnlem2  22768  logcnlem3  22769  logcnlem4  22770  logtayllem  22784  logtayl  22785  cxpcl  22799  recxpcl  22800  leibpilem2  23016  leibpi  23017  rlimcnp2  23040  efrlim  23043  pclogsum  23234  dchrelbasd  23258  lgsfcl2  23321  lgscllem  23322  lgsval2lem  23325  lgsne0  23352  dchrvmasumiflem1  23430  dchrvmasumiflem2  23431  dchrisum0flblem1  23437  pntrlog2bndlem4  23509  pntrlog2bndlem5  23510  pntlemj  23532  padicabv  23559  sgnsval  27396  xrge0iifcnv  27567  xrge0iifhom  27571  pnfneige0  27585  esumpinfval  27735  sigaclfu2  27777  ballotlemsv  28104  ballotlemsdom  28106  signsvvf  28192  signsvfn  28195  igamf  28249  igamcl  28250  itg2addnclem2  29660  itg2gt0cn  29663  ibladdnclem  29664  itgaddnclem1  29666  iblabsnclem  29671  iblabsnc  29672  iblmulc2nc  29673  itgmulc2nclem1  29674  bddiblnc  29678  itggt0cn  29680  ftc1anclem5  29687  ftc1anclem6  29688  ftc1anclem7  29689  ftc1anclem8  29690  ftc1anc  29691  areacirc  29705  sdrgacs  30771  ioondisj2  31105  ioondisj1  31106  climsuse  31166  lptioo2  31189  lptioo1  31190  icccncfext  31242  cncfiooicclem1  31248  iblsplit  31300  dirkerval2  31410  dirkerre  31411  lincext1  32145  cdleme27cl  35171
  Copyright terms: Public domain W3C validator