MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplbi Structured version   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  sbequ2  1660  reurex  2922  eqimss  3400  pssss  3442  eldifi  3469  inss1  3561  ssunsn2  3958  pwssun  4489  sopo  4520  wefr  4572  ordtr  4595  opelxp1  4911  relop  5023  funmo  5470  funrel  5471  fnfun  5542  ffn  5591  f1f  5639  f1of1  5673  f1ofo  5681  isof1o  6045  eqopi  6383  1st2nd2  6386  reldmtpos  6487  swoer  6933  erdisj  6952  ecopover  7008  sdomdom  7135  inf3lemd  7582  mapfien  7653  cardprclem  7866  infxpenlem  7895  cardinfima  7978  dfac5lem4  8007  domtriomlem  8322  smobeth  8461  fpwwe2lem6  8510  fpwwe2lem7  8511  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwe2  8518  axrnegex  9037  axpre-sup  9044  zre  10286  nnssz  10301  ixxss1  10934  ixxss2  10935  ixxss12  10936  lbioo  10947  ubioo  10948  iccss2  10981  elfzuz  11055  uzdisj  11119  splfv1  11784  sqrlem6  12053  rlimf  12295  lo1f  12312  lo1dm  12313  o1f  12323  o1dm  12324  fsumge0  12574  mertenslem2  12662  divalglem9  12921  bitsinv2  12955  bitsf1ocnv  12956  gcdcllem1  13011  prmnn  13082  prmind2  13090  nprm  13093  prmuz2  13097  isprm6  13109  exprmfct  13110  isprm5  13112  maxprmfct  13113  phibndlem  13159  phibnd  13160  dfphi2  13163  phimullem  13168  pclem  13212  pcprendvds2  13215  pcpre1  13216  expnprm  13271  prmreclem1  13284  1arith  13295  4sqlem15  13327  4sqlem16  13328  vdwlem5  13353  vdwlem6  13354  vdwlem8  13356  vdwlem9  13357  vdwlem11  13359  ramtlecl  13368  0ramcl  13391  firest  13660  acsmre  13877  posprs  14406  latpos  14478  dlatl  14621  pslem  14638  tsrlemax  14652  tsrps  14653  laps  14668  mndlem1  14694  grpmnd  14817  nsgsubg  14972  ghmgrp1  15008  ghmgrp2  15009  gimghm  15051  gagrp  15069  gaset  15070  efgredeu  15384  ablgrp  15417  cmnmnd  15427  cyggenod2  15495  cyggrp  15499  ablfac2  15647  crngrng  15674  dvdsrcl  15754  unitcl  15764  drngrng  15842  subrgrng  15871  subrgrcl  15873  srngrhm  15939  lmimlmhm  16136  lveclmod  16178  2idlcpbl  16305  divs1  16306  divsrhm  16308  lpirrng  16323  nzrrng  16332  domnnzr  16355  fldidom  16365  assalmod  16379  assarng  16380  assasca  16381  cygznlem1  16847  cygznlem3  16850  topontop  16991  tpstop  17004  clsval2  17114  mretopd  17156  neiptoptop  17195  perftop  17220  restfpw  17243  cntop1  17304  cntop2  17305  cnptop1  17306  cnptop2  17307  cnprcl  17309  t1ficld  17391  t0top  17393  t1top  17394  haustop  17395  regtop  17397  nrmtop  17400  cnrmtop  17401  pnrmnrm  17404  cmptop  17458  discmp  17461  tgcmp  17464  uncmp  17466  conndisj  17479  contop  17480  1stctop  17506  llytop  17535  nllytop  17536  hmeocn  17792  filfbas  17880  ufilfil  17936  flimtop  17997  flimfil  18001  alexsublem  18075  ptcmplem3  18085  tsmsfbas  18157  tsmslem1  18158  tsmsgsum  18168  tsmssubm  18172  tsmsres  18173  tsmsf1o  18174  tsmsmhm  18175  tsmsadd  18176  tsmsxplem1  18182  tsmsxplem2  18183  tsmsxp  18184  tlmtmd  18216  tlmlmod  18218  tlmtrg  18219  tvctlm  18226  ressust  18294  uspreg  18304  ucncn  18315  neipcfilu  18326  cuspusp  18330  isxmet2d  18357  metxmet  18364  xmstps  18483  msxms  18484  xmsxmet  18486  msmet  18487  stdbdxmet  18545  nrgngp  18698  nlmngp  18713  nlmlmod  18714  nlmnrg  18715  nvcnlm  18731  nmoi  18762  nghmrcl1  18766  nghmrcl2  18767  nmhmrcl1  18781  nmhmrcl2  18782  qdensere  18804  xrge0gsumle  18864  xrge0tsms  18865  metds0  18880  metdstri  18881  metdsre  18883  metdseq0  18884  metdscnlem  18885  metnrmlem1a  18888  metnrmlem1  18889  icopnfcnv  18967  icopnfhmeo  18968  cmetmet  19239  cmsms  19301  hlbn  19317  ovolicc1  19412  ovolicc2lem5  19417  mblss  19427  mbff  19519  mbfres  19536  mbfadd  19553  mbfsub  19554  i1fmbf  19567  mbfmul  19618  bddmulibl  19730  limcmpt  19770  c1liplem1  19880  c1lip2  19882  fta1glem1  20088  fta1glem2  20089  fta1g  20090  fta1b  20092  ply1pid  20102  aacn  20234  ulmf2  20300  logdmnrp  20532  logdmss  20533  logcnlem2  20534  logcnlem3  20535  logcnlem4  20536  logcnlem5  20537  logcn  20538  dvloglem  20539  logf1o2  20541  efopnlem1  20547  logtayl2  20553  cxpcn  20629  cxpcn3lem  20631  cxpcn3  20632  resqrcn  20633  atandmneg  20746  atandmcj  20749  cosatan  20761  cosatanne0  20762  birthdaylem1  20790  areacl  20801  cxp2lim  20815  jensenlem2  20826  jensen  20827  wilth  20854  sqff1o  20965  dvdsmulf1o  20979  mersenne  21011  bposlem3  21070  lgsqrlem1  21125  lgsqrlem2  21126  lgsqrlem3  21127  lgsqrlem4  21128  lgseisenlem3  21135  lgsquad2lem2  21143  2sqlem6  21153  chebbnd1  21166  chtppilim  21169  chpchtlim  21173  chpo1ub  21174  rplogsumlem1  21178  rplogsumlem2  21179  dchrmusumlema  21187  dchrvmasumiflem1  21195  dchrisum0flblem2  21203  dchrisum0lema  21208  dchrisum0lem2  21212  selberg3lem2  21252  pntrsumo1  21259  selbergsb  21269  pnt2  21307  ostthlem2  21322  ostth2lem2  21328  uhgra0v  21345  usgra0v  21391  usgra1v  21409  eupagra  21688  ablogrpo  21872  smgrpismgm  21920  mndoissmgrp  21927  nmogtmnf  22271  bnnv  22368  hlobn  22390  hcauseq  22687  hlimseqi  22691  hlimveci  22692  shss  22712  sh0  22718  chsh  22727  lnopf  23362  bdopln  23364  nmopgtmnf  23371  hmopf  23377  lnfnf  23387  unopf1o  23419  elunop2  23516  elpjhmop  23688  stcltrlem1  23779  mdslle1i  23820  mdslle2i  23821  rabexgfGS  23987  ssnnssfz  24148  tospos  24186  xrge0tsmsd  24223  ofldsqr  24240  ofldlt1  24243  ofldchr  24244  lmxrge0  24337  qqhrhm  24373  esumpcvgval  24468  measssd  24569  elmbfmvol2  24617  domprobmeas  24668  ballotlemscr  24776  ballotlemfg  24783  ballotlemfrc  24784  ballotlemfrceq  24786  ballotlemrinv0  24790  subfacval3  24875  pcontop  24912  sconpcon  24914  cvmcn  24949  cvmliftlem10  24981  fundmpss  25390  predel  25458  sltres  25619  funpartfun  25788  axcontlem2  25904  axcontlem7  25909  axcontlem8  25910  axcontlem10  25912  outsideofcol  26067  itg2addnc  26259  itg2gt0cn  26260  ftc1anclem3  26282  fnebas  26353  filnetlem3  26409  istotbnd3  26480  totbndmet  26481  sstotbnd2  26483  sstotbnd  26484  equivtotbnd  26487  bndmet  26490  totbndbnd  26498  prdstotbnd  26503  crngorngo  26610  prrngorngo  26661  divrngpr  26663  an3  26697  nacsacs  26763  eldiophelnn0  26822  jm2.17a  27025  jm2.17b  27026  jm2.17c  27027  jm2.27c  27078  jm3.1lem1  27088  jm3.1lem2  27089  jm3.1lem3  27090  lnmlmod  27154  lbslinds  27280  lnrrng  27293  mncply  27319  psgneu  27406  idomrootle  27488  idomodle  27489  hashgcdlem  27493  stoweidlem14  27739  stoweidlem16  27741  stoweidlem24  27749  stoweidlem39  27764  stoweidlem50  27775  stoweidlem51  27776  stoweidlem54  27779  stoweidlem57  27782  wallispilem3  27792  ndmafv  27980  frgrawopreg  28438  2uasbanh  28648  bnj563  29111  bnj658  29119  bnj667  29120  bnj570  29276  bnj938  29308  bnj1001  29329  bnj1006  29330  bnj1049  29343  bnj1121  29354  bnj1173  29371  bnj1177  29375  bnj1245  29383  bnj1311  29393  bnj1321  29396  bnj1388  29402  bnj1398  29403  bnj1415  29407  bnj1417  29410  bnj1421  29411  bnj1442  29418  bnj1452  29421  bnj1489  29425  bnj1312  29427  ollat  30011  omlol  30038  cvlatl  30123  hlomcmcv  30154  2dim  30267  1dimN  30268  lcfl8b  32302  lclkrlem2  32330  lclkrslem1  32335  lclkrslem2  32336  lcfrlem9  32348  mapdval2N  32428  mapdordlem2  32435  mapdrvallem2  32443
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