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

Theorem simplbi 446
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simplbi.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simplbi  |-  ( ph  ->  ps )

Proof of Theorem simplbi
StepHypRef Expression
1 simplbi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpi 186 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simpld 445 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  3simpa  952  reurex  2754  eqimss  3230  pssss  3271  eldifi  3298  inss1  3389  ssunsn2  3773  pwssun  4299  sopo  4331  wefr  4383  ordtr  4406  opelxp1  4722  relop  4834  funmo  5271  funrel  5272  fnfun  5341  ffn  5389  f1f  5437  f1of1  5471  f1ofo  5479  isof1o  5822  eqopi  6156  1st2nd2  6159  reldmtpos  6242  swoer  6688  erdisj  6707  ecopover  6762  sdomdom  6889  inf3lemd  7328  mapfien  7399  cardprclem  7612  infxpenlem  7641  cardinfima  7724  dfac5lem4  7753  domtriomlem  8068  smobeth  8208  fpwwe2lem6  8257  fpwwe2lem7  8258  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  axrnegex  8784  axpre-sup  8791  eqlei  8942  zre  10028  nnssz  10043  supminf  10305  ixxss1  10674  ixxss2  10675  ixxss12  10676  lbioo  10687  ubioo  10688  iccss2  10720  elfzuz  10794  uzdisj  10856  splfv1  11470  sqrlem6  11733  rlimf  11975  lo1f  11992  lo1dm  11993  o1f  12003  o1dm  12004  fsumge0  12253  incexc2  12297  mertenslem2  12341  divalglem9  12600  bitsinv2  12634  bitsf1ocnv  12635  gcdcllem1  12690  prmnn  12761  prmind2  12769  nprm  12772  prmuz2  12776  isprm6  12788  exprmfct  12789  isprm5  12791  maxprmfct  12792  phibndlem  12838  phibnd  12839  dfphi2  12842  phimullem  12847  pclem  12891  pcprendvds2  12894  pcpre1  12895  expnprm  12950  prmreclem1  12963  1arith  12974  4sqlem15  13006  4sqlem16  13007  vdwlem5  13032  vdwlem6  13033  vdwlem8  13035  vdwlem9  13036  vdwlem11  13038  ramtlecl  13047  0ramcl  13070  firest  13337  acsmre  13554  posprs  14083  latpos  14155  dlatl  14298  pslem  14315  tsrlemax  14329  tsrps  14330  laps  14345  mndlem1  14371  grpmnd  14494  nsgsubg  14649  ghmgrp1  14685  ghmgrp2  14686  gimghm  14728  gagrp  14746  gaset  14747  efgredeu  15061  ablgrp  15094  cmnmnd  15104  cyggenod2  15172  cyggrp  15176  ablfac2  15324  crngrng  15351  dvdsrcl  15431  unitcl  15441  drngrng  15519  subrgrng  15548  subrgrcl  15550  srngrhm  15616  lmimlmhm  15817  lveclmod  15859  2idlcpbl  15986  divs1  15987  divsrhm  15989  lpirrng  16004  nzrrng  16013  domnnzr  16036  fldidom  16046  assalmod  16060  assarng  16061  assasca  16062  cygznlem1  16520  cygznlem3  16523  topontop  16664  tpstop  16677  clsval2  16787  mretopd  16829  perftop  16887  restfpw  16910  cntop1  16970  cntop2  16971  cnptop1  16972  cnptop2  16973  cnprcl  16975  t1ficld  17055  t0top  17057  t1top  17058  haustop  17059  regtop  17061  nrmtop  17064  cnrmtop  17065  pnrmnrm  17068  cmptop  17122  discmp  17125  tgcmp  17128  uncmp  17130  conndisj  17142  contop  17143  1stctop  17169  llytop  17198  nllytop  17199  txdis1cn  17329  hmeocn  17451  filfbas  17543  ufilfil  17599  flimtop  17660  flimfil  17664  alexsublem  17738  ptcmplem3  17748  tsmsfbas  17810  tsmslem1  17811  tsmsgsum  17821  tsmssubm  17825  tsmsres  17826  tsmsf1o  17827  tsmsmhm  17828  tsmsadd  17829  tsmsxplem1  17835  tsmsxplem2  17836  tsmsxp  17837  tlmtmd  17869  tlmlmod  17871  tlmtrg  17872  tvctlm  17879  isxmet2d  17892  metxmet  17899  xmstps  17999  msxms  18000  xmsxmet  18002  msmet  18003  stdbdxmet  18061  nrgngp  18173  nlmngp  18188  nlmlmod  18189  nlmnrg  18190  nvcnlm  18206  nmoi  18237  nghmrcl1  18241  nghmrcl2  18242  nmhmrcl1  18256  nmhmrcl2  18257  qdensere  18279  xrge0gsumle  18338  xrge0tsms  18339  metds0  18354  metdstri  18355  metdsre  18357  metdseq0  18358  metdscnlem  18359  metnrmlem1a  18362  metnrmlem1  18363  icopnfcnv  18440  icopnfhmeo  18441  cmetmet  18712  cmsms  18770  hlbn  18780  ovolicc1  18875  ovolicc2lem5  18880  mblss  18890  mbff  18982  mbfres  18999  mbfadd  19016  mbfsub  19017  i1fmbf  19030  mbfmul  19081  bddmulibl  19193  limcmpt  19233  dvcnvlem  19323  c1liplem1  19343  c1lip2  19345  fta1glem1  19551  fta1glem2  19552  fta1g  19553  fta1b  19555  ply1pid  19565  aacn  19697  ulmf2  19763  logdmnrp  19988  logdmss  19989  logcnlem2  19990  logcnlem3  19991  logcnlem4  19992  logcnlem5  19993  logcn  19994  dvloglem  19995  logf1o2  19997  efopnlem1  20003  logtayl2  20009  cxpcn  20085  cxpcn3lem  20087  cxpcn3  20088  resqrcn  20089  atandmneg  20202  atandmcj  20205  cosatan  20217  cosatanne0  20218  birthdaylem1  20246  areacl  20257  cxp2lim  20271  jensenlem2  20282  jensen  20283  wilth  20309  sqff1o  20420  dvdsdivcl  20421  fsumdvdsdiaglem  20423  dvdsflf1o  20427  muinv  20433  dvdsmulf1o  20434  mersenne  20466  bposlem3  20525  lgsqrlem1  20580  lgsqrlem2  20581  lgsqrlem3  20582  lgsqrlem4  20583  lgseisenlem3  20590  lgsquad2lem2  20598  2sqlem6  20608  chebbnd1  20621  chtppilim  20624  chpchtlim  20628  chpo1ub  20629  rplogsumlem1  20633  rplogsumlem2  20634  dchrmusumlema  20642  dchrvmasumiflem1  20650  dchrisum0flblem2  20658  dchrisum0lema  20663  dchrisum0lem2  20667  logsqvma  20691  selberg3lem2  20707  pntrsumo1  20714  selbergsb  20724  pnt2  20762  ostthlem2  20777  ostth2lem2  20783  ablogrpo  20951  smgrpismgm  20999  mndoissmgrp  21006  nmogtmnf  21348  bnnv  21445  hlobn  21467  hcauseq  21764  hlimseqi  21768  hlimveci  21769  shss  21789  sh0  21795  chsh  21804  lnopf  22439  bdopln  22441  nmopgtmnf  22448  hmopf  22454  lnfnf  22464  unopf1o  22496  elunop2  22593  elpjhmop  22765  stcltrlem1  22856  mdslle1i  22897  mdslle2i  22898  ballotlemfc0  23051  ballotlemfcc  23052  ballotlem5  23058  ballotlemscr  23077  ballotlemfg  23084  ballotlemfrc  23085  ballotlemfrceq  23087  ballotlemrinv0  23091  rabexgfGS  23171  ssnnssfz  23277  lmxrge0  23375  xrge0tsmsd  23382  esumpcvgval  23446  insiga  23498  brsiga  23514  measssd  23543  measinb2  23550  pwcntmeas  23554  mbfmbfm  23563  imambfm  23567  elmbfmvol2  23572  mbfmcnt  23573  domprobmeas  23613  cndprob01  23638  isrrvv  23646  dstrvprob  23672  subfacval3  23720  pcontop  23756  sconpcon  23758  cvmcn  23793  cvmliftlem10  23825  eupagra  23882  fundmpss  24122  predel  24183  sltres  24318  funpartfun  24481  axcontlem2  24593  axcontlem7  24598  axcontlem8  24599  axcontlem10  24601  outsideofcol  24756  fordisxex  24954  alneal1  25000  dfdir2  25291  dirpre  25293  isibg1a  26111  fnebas  26273  filnetlem3  26329  istotbnd3  26495  totbndmet  26496  sstotbnd2  26498  sstotbnd  26499  equivtotbnd  26502  bndmet  26505  totbndbnd  26513  prdstotbnd  26518  crngorngo  26625  prrngorngo  26676  divrngpr  26678  an3  26714  nacsacs  26784  eldiophelnn0  26843  jm2.17a  27047  jm2.17b  27048  jm2.17c  27049  jm2.27c  27100  jm3.1lem1  27110  jm3.1lem2  27111  jm3.1lem3  27112  lnmlmod  27177  lbslinds  27303  lnrrng  27316  mncply  27342  psgneu  27429  idomrootle  27511  idomodle  27512  hashgcdlem  27516  fnvinran  27685  cncmpmax  27703  stoweidlem14  27763  stoweidlem16  27765  stoweidlem24  27773  stoweidlem39  27788  stoweidlem50  27799  stoweidlem54  27803  stoweidlem57  27806  wallispilem3  27816  ndmafv  28003  usgra0v  28117  usgra1v  28126  uvtxisvtx  28162  2uasbanh  28327  bnj563  28772  bnj658  28780  bnj667  28781  bnj570  28937  bnj938  28969  bnj1001  28990  bnj1006  28991  bnj1049  29004  bnj1121  29015  bnj1173  29032  bnj1177  29036  bnj1245  29044  bnj1311  29054  bnj1321  29057  bnj1388  29063  bnj1398  29064  bnj1415  29068  bnj1417  29071  bnj1421  29072  bnj1442  29079  bnj1452  29082  bnj1489  29086  bnj1312  29088  ollat  29403  omlol  29430  cvlatl  29515  hlomcmcv  29546  2dim  29659  1dimN  29660  lcfl8b  31694  lclkrlem2  31722  lclkrslem1  31727  lclkrslem2  31728  lcfrlem9  31740  mapdval2N  31820  mapdordlem2  31827  mapdrvallem2  31835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator