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

Theorem simplbi 447
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 187 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simpld 446 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  3simpa  954  reurex  2865  eqimss  3343  pssss  3385  eldifi  3412  inss1  3504  ssunsn2  3901  pwssun  4430  sopo  4461  wefr  4513  ordtr  4536  opelxp1  4851  relop  4963  funmo  5410  funrel  5411  fnfun  5482  ffn  5531  f1f  5579  f1of1  5613  f1ofo  5621  isof1o  5984  eqopi  6322  1st2nd2  6325  reldmtpos  6423  swoer  6869  erdisj  6888  ecopover  6944  sdomdom  7071  inf3lemd  7515  mapfien  7586  cardprclem  7799  infxpenlem  7828  cardinfima  7911  dfac5lem4  7940  domtriomlem  8255  smobeth  8394  fpwwe2lem6  8443  fpwwe2lem7  8444  fpwwe2lem12  8449  fpwwe2lem13  8450  fpwwe2  8451  axrnegex  8970  axpre-sup  8977  eqlei  9128  zre  10218  nnssz  10233  ixxss1  10866  ixxss2  10867  ixxss12  10868  lbioo  10879  ubioo  10880  iccss2  10913  elfzuz  10987  uzdisj  11049  splfv1  11711  sqrlem6  11980  rlimf  12222  lo1f  12239  lo1dm  12240  o1f  12250  o1dm  12251  fsumge0  12501  mertenslem2  12589  divalglem9  12848  bitsinv2  12882  bitsf1ocnv  12883  gcdcllem1  12938  prmnn  13009  prmind2  13017  nprm  13020  prmuz2  13024  isprm6  13036  exprmfct  13037  isprm5  13039  maxprmfct  13040  phibndlem  13086  phibnd  13087  dfphi2  13090  phimullem  13095  pclem  13139  pcprendvds2  13142  pcpre1  13143  expnprm  13198  prmreclem1  13211  1arith  13222  4sqlem15  13254  4sqlem16  13255  vdwlem5  13280  vdwlem6  13281  vdwlem8  13283  vdwlem9  13284  vdwlem11  13286  ramtlecl  13295  0ramcl  13318  firest  13587  acsmre  13804  posprs  14333  latpos  14405  dlatl  14548  pslem  14565  tsrlemax  14579  tsrps  14580  laps  14595  mndlem1  14621  grpmnd  14744  nsgsubg  14899  ghmgrp1  14935  ghmgrp2  14936  gimghm  14978  gagrp  14996  gaset  14997  efgredeu  15311  ablgrp  15344  cmnmnd  15354  cyggenod2  15422  cyggrp  15426  ablfac2  15574  crngrng  15601  dvdsrcl  15681  unitcl  15691  drngrng  15769  subrgrng  15798  subrgrcl  15800  srngrhm  15866  lmimlmhm  16063  lveclmod  16105  2idlcpbl  16232  divs1  16233  divsrhm  16235  lpirrng  16250  nzrrng  16259  domnnzr  16282  fldidom  16292  assalmod  16306  assarng  16307  assasca  16308  cygznlem1  16770  cygznlem3  16773  topontop  16914  tpstop  16927  clsval2  17037  mretopd  17079  neiptoptop  17118  perftop  17142  restfpw  17165  cntop1  17226  cntop2  17227  cnptop1  17228  cnptop2  17229  cnprcl  17231  t1ficld  17313  t0top  17315  t1top  17316  haustop  17317  regtop  17319  nrmtop  17322  cnrmtop  17323  pnrmnrm  17326  cmptop  17380  discmp  17383  tgcmp  17386  uncmp  17388  conndisj  17400  contop  17401  1stctop  17427  llytop  17456  nllytop  17457  hmeocn  17713  filfbas  17801  ufilfil  17857  flimtop  17918  flimfil  17922  alexsublem  17996  ptcmplem3  18006  tsmsfbas  18078  tsmslem1  18079  tsmsgsum  18089  tsmssubm  18093  tsmsres  18094  tsmsf1o  18095  tsmsmhm  18096  tsmsadd  18097  tsmsxplem1  18103  tsmsxplem2  18104  tsmsxp  18105  tlmtmd  18137  tlmlmod  18139  tlmtrg  18140  tvctlm  18147  ressust  18215  uspreg  18225  ucncn  18236  neipcfilu  18247  cuspusp  18251  isxmet2d  18266  metxmet  18273  xmstps  18373  msxms  18374  xmsxmet  18376  msmet  18377  stdbdxmet  18435  nrgngp  18569  nlmngp  18584  nlmlmod  18585  nlmnrg  18586  nvcnlm  18602  nmoi  18633  nghmrcl1  18637  nghmrcl2  18638  nmhmrcl1  18652  nmhmrcl2  18653  qdensere  18675  xrge0gsumle  18735  xrge0tsms  18736  metds0  18751  metdstri  18752  metdsre  18754  metdseq0  18755  metdscnlem  18756  metnrmlem1a  18759  metnrmlem1  18760  icopnfcnv  18838  icopnfhmeo  18839  cmetmet  19110  cmsms  19170  hlbn  19184  ovolicc1  19279  ovolicc2lem5  19284  mblss  19294  mbff  19386  mbfres  19403  mbfadd  19420  mbfsub  19421  i1fmbf  19434  mbfmul  19485  bddmulibl  19597  limcmpt  19637  c1liplem1  19747  c1lip2  19749  fta1glem1  19955  fta1glem2  19956  fta1g  19957  fta1b  19959  ply1pid  19969  aacn  20101  ulmf2  20167  logdmnrp  20399  logdmss  20400  logcnlem2  20401  logcnlem3  20402  logcnlem4  20403  logcnlem5  20404  logcn  20405  dvloglem  20406  logf1o2  20408  efopnlem1  20414  logtayl2  20420  cxpcn  20496  cxpcn3lem  20498  cxpcn3  20499  resqrcn  20500  atandmneg  20613  atandmcj  20616  cosatan  20628  cosatanne0  20629  birthdaylem1  20657  areacl  20668  cxp2lim  20682  jensenlem2  20693  jensen  20694  wilth  20721  sqff1o  20832  dvdsmulf1o  20846  mersenne  20878  bposlem3  20937  lgsqrlem1  20992  lgsqrlem2  20993  lgsqrlem3  20994  lgsqrlem4  20995  lgseisenlem3  21002  lgsquad2lem2  21010  2sqlem6  21020  chebbnd1  21033  chtppilim  21036  chpchtlim  21040  chpo1ub  21041  rplogsumlem1  21045  rplogsumlem2  21046  dchrmusumlema  21054  dchrvmasumiflem1  21062  dchrisum0flblem2  21070  dchrisum0lema  21075  dchrisum0lem2  21079  selberg3lem2  21119  pntrsumo1  21126  selbergsb  21136  pnt2  21174  ostthlem2  21189  ostth2lem2  21195  uhgra0v  21212  usgra0v  21258  usgra1v  21275  eupagra  21536  ablogrpo  21720  smgrpismgm  21768  mndoissmgrp  21775  nmogtmnf  22119  bnnv  22216  hlobn  22238  hcauseq  22535  hlimseqi  22539  hlimveci  22540  shss  22560  sh0  22566  chsh  22575  lnopf  23210  bdopln  23212  nmopgtmnf  23219  hmopf  23225  lnfnf  23235  unopf1o  23267  elunop2  23364  elpjhmop  23536  stcltrlem1  23627  mdslle1i  23668  mdslle2i  23669  rabexgfGS  23831  ssnnssfz  23984  tospos  24025  xrge0tsmsd  24052  ofldsqr  24066  ofldlt1  24069  ofldchr  24070  lmxrge0  24141  qqhrhm  24172  esumpcvgval  24264  measssd  24363  elmbfmvol2  24411  domprobmeas  24447  ballotlemscr  24555  ballotlemfg  24562  ballotlemfrc  24563  ballotlemfrceq  24565  ballotlemrinv0  24569  subfacval3  24654  pcontop  24691  sconpcon  24693  cvmcn  24728  cvmliftlem10  24760  fundmpss  25146  predel  25207  sltres  25342  funpartfun  25506  axcontlem2  25618  axcontlem7  25623  axcontlem8  25624  axcontlem10  25626  outsideofcol  25781  itg2gt0cn  25960  fnebas  26044  filnetlem3  26100  istotbnd3  26171  totbndmet  26172  sstotbnd2  26174  sstotbnd  26175  equivtotbnd  26178  bndmet  26181  totbndbnd  26189  prdstotbnd  26194  crngorngo  26301  prrngorngo  26352  divrngpr  26354  an3  26388  nacsacs  26454  eldiophelnn0  26513  jm2.17a  26716  jm2.17b  26717  jm2.17c  26718  jm2.27c  26769  jm3.1lem1  26779  jm3.1lem2  26780  jm3.1lem3  26781  lnmlmod  26846  lbslinds  26972  lnrrng  26985  mncply  27011  psgneu  27098  idomrootle  27180  idomodle  27181  hashgcdlem  27185  stoweidlem14  27431  stoweidlem16  27433  stoweidlem24  27441  stoweidlem39  27456  stoweidlem50  27467  stoweidlem51  27468  stoweidlem54  27471  stoweidlem57  27474  wallispilem3  27484  ndmafv  27673  frgrawopreg  27801  2uasbanh  27991  bnj563  28449  bnj658  28457  bnj667  28458  bnj570  28614  bnj938  28646  bnj1001  28667  bnj1006  28668  bnj1049  28681  bnj1121  28692  bnj1173  28709  bnj1177  28713  bnj1245  28721  bnj1311  28731  bnj1321  28734  bnj1388  28740  bnj1398  28741  bnj1415  28745  bnj1417  28748  bnj1421  28749  bnj1442  28756  bnj1452  28759  bnj1489  28763  bnj1312  28765  ollat  29328  omlol  29355  cvlatl  29440  hlomcmcv  29471  2dim  29584  1dimN  29585  lcfl8b  31619  lclkrlem2  31647  lclkrslem1  31652  lclkrslem2  31653  lcfrlem9  31665  mapdval2N  31745  mapdordlem2  31752  mapdrvallem2  31760
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 178  df-an 361
  Copyright terms: Public domain W3C validator