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  2914  eqimss  3392  pssss  3434  eldifi  3461  inss1  3553  ssunsn2  3950  pwssun  4481  sopo  4512  wefr  4564  ordtr  4587  opelxp1  4903  relop  5015  funmo  5462  funrel  5463  fnfun  5534  ffn  5583  f1f  5631  f1of1  5665  f1ofo  5673  isof1o  6037  eqopi  6375  1st2nd2  6378  reldmtpos  6479  swoer  6925  erdisj  6944  ecopover  7000  sdomdom  7127  inf3lemd  7574  mapfien  7645  cardprclem  7858  infxpenlem  7887  cardinfima  7970  dfac5lem4  7999  domtriomlem  8314  smobeth  8453  fpwwe2lem6  8502  fpwwe2lem7  8503  fpwwe2lem12  8508  fpwwe2lem13  8509  fpwwe2  8510  axrnegex  9029  axpre-sup  9036  zre  10278  nnssz  10293  ixxss1  10926  ixxss2  10927  ixxss12  10928  lbioo  10939  ubioo  10940  iccss2  10973  elfzuz  11047  uzdisj  11111  splfv1  11776  sqrlem6  12045  rlimf  12287  lo1f  12304  lo1dm  12305  o1f  12315  o1dm  12316  fsumge0  12566  mertenslem2  12654  divalglem9  12913  bitsinv2  12947  bitsf1ocnv  12948  gcdcllem1  13003  prmnn  13074  prmind2  13082  nprm  13085  prmuz2  13089  isprm6  13101  exprmfct  13102  isprm5  13104  maxprmfct  13105  phibndlem  13151  phibnd  13152  dfphi2  13155  phimullem  13160  pclem  13204  pcprendvds2  13207  pcpre1  13208  expnprm  13263  prmreclem1  13276  1arith  13287  4sqlem15  13319  4sqlem16  13320  vdwlem5  13345  vdwlem6  13346  vdwlem8  13348  vdwlem9  13349  vdwlem11  13351  ramtlecl  13360  0ramcl  13383  firest  13652  acsmre  13869  posprs  14398  latpos  14470  dlatl  14613  pslem  14630  tsrlemax  14644  tsrps  14645  laps  14660  mndlem1  14686  grpmnd  14809  nsgsubg  14964  ghmgrp1  15000  ghmgrp2  15001  gimghm  15043  gagrp  15061  gaset  15062  efgredeu  15376  ablgrp  15409  cmnmnd  15419  cyggenod2  15487  cyggrp  15491  ablfac2  15639  crngrng  15666  dvdsrcl  15746  unitcl  15756  drngrng  15834  subrgrng  15863  subrgrcl  15865  srngrhm  15931  lmimlmhm  16128  lveclmod  16170  2idlcpbl  16297  divs1  16298  divsrhm  16300  lpirrng  16315  nzrrng  16324  domnnzr  16347  fldidom  16357  assalmod  16371  assarng  16372  assasca  16373  cygznlem1  16839  cygznlem3  16842  topontop  16983  tpstop  16996  clsval2  17106  mretopd  17148  neiptoptop  17187  perftop  17212  restfpw  17235  cntop1  17296  cntop2  17297  cnptop1  17298  cnptop2  17299  cnprcl  17301  t1ficld  17383  t0top  17385  t1top  17386  haustop  17387  regtop  17389  nrmtop  17392  cnrmtop  17393  pnrmnrm  17396  cmptop  17450  discmp  17453  tgcmp  17456  uncmp  17458  conndisj  17471  contop  17472  1stctop  17498  llytop  17527  nllytop  17528  hmeocn  17784  filfbas  17872  ufilfil  17928  flimtop  17989  flimfil  17993  alexsublem  18067  ptcmplem3  18077  tsmsfbas  18149  tsmslem1  18150  tsmsgsum  18160  tsmssubm  18164  tsmsres  18165  tsmsf1o  18166  tsmsmhm  18167  tsmsadd  18168  tsmsxplem1  18174  tsmsxplem2  18175  tsmsxp  18176  tlmtmd  18208  tlmlmod  18210  tlmtrg  18211  tvctlm  18218  ressust  18286  uspreg  18296  ucncn  18307  neipcfilu  18318  cuspusp  18322  isxmet2d  18349  metxmet  18356  xmstps  18475  msxms  18476  xmsxmet  18478  msmet  18479  stdbdxmet  18537  nrgngp  18690  nlmngp  18705  nlmlmod  18706  nlmnrg  18707  nvcnlm  18723  nmoi  18754  nghmrcl1  18758  nghmrcl2  18759  nmhmrcl1  18773  nmhmrcl2  18774  qdensere  18796  xrge0gsumle  18856  xrge0tsms  18857  metds0  18872  metdstri  18873  metdsre  18875  metdseq0  18876  metdscnlem  18877  metnrmlem1a  18880  metnrmlem1  18881  icopnfcnv  18959  icopnfhmeo  18960  cmetmet  19231  cmsms  19293  hlbn  19309  ovolicc1  19404  ovolicc2lem5  19409  mblss  19419  mbff  19511  mbfres  19528  mbfadd  19545  mbfsub  19546  i1fmbf  19559  mbfmul  19610  bddmulibl  19722  limcmpt  19762  c1liplem1  19872  c1lip2  19874  fta1glem1  20080  fta1glem2  20081  fta1g  20082  fta1b  20084  ply1pid  20094  aacn  20226  ulmf2  20292  logdmnrp  20524  logdmss  20525  logcnlem2  20526  logcnlem3  20527  logcnlem4  20528  logcnlem5  20529  logcn  20530  dvloglem  20531  logf1o2  20533  efopnlem1  20539  logtayl2  20545  cxpcn  20621  cxpcn3lem  20623  cxpcn3  20624  resqrcn  20625  atandmneg  20738  atandmcj  20741  cosatan  20753  cosatanne0  20754  birthdaylem1  20782  areacl  20793  cxp2lim  20807  jensenlem2  20818  jensen  20819  wilth  20846  sqff1o  20957  dvdsmulf1o  20971  mersenne  21003  bposlem3  21062  lgsqrlem1  21117  lgsqrlem2  21118  lgsqrlem3  21119  lgsqrlem4  21120  lgseisenlem3  21127  lgsquad2lem2  21135  2sqlem6  21145  chebbnd1  21158  chtppilim  21161  chpchtlim  21165  chpo1ub  21166  rplogsumlem1  21170  rplogsumlem2  21171  dchrmusumlema  21179  dchrvmasumiflem1  21187  dchrisum0flblem2  21195  dchrisum0lema  21200  dchrisum0lem2  21204  selberg3lem2  21244  pntrsumo1  21251  selbergsb  21261  pnt2  21299  ostthlem2  21314  ostth2lem2  21320  uhgra0v  21337  usgra0v  21383  usgra1v  21401  eupagra  21680  ablogrpo  21864  smgrpismgm  21912  mndoissmgrp  21919  nmogtmnf  22263  bnnv  22360  hlobn  22382  hcauseq  22679  hlimseqi  22683  hlimveci  22684  shss  22704  sh0  22710  chsh  22719  lnopf  23354  bdopln  23356  nmopgtmnf  23363  hmopf  23369  lnfnf  23379  unopf1o  23411  elunop2  23508  elpjhmop  23680  stcltrlem1  23771  mdslle1i  23812  mdslle2i  23813  rabexgfGS  23979  ssnnssfz  24140  tospos  24178  xrge0tsmsd  24215  ofldsqr  24232  ofldlt1  24235  ofldchr  24236  lmxrge0  24329  qqhrhm  24365  esumpcvgval  24460  measssd  24561  elmbfmvol2  24609  domprobmeas  24660  ballotlemscr  24768  ballotlemfg  24775  ballotlemfrc  24776  ballotlemfrceq  24778  ballotlemrinv0  24782  subfacval3  24867  pcontop  24904  sconpcon  24906  cvmcn  24941  cvmliftlem10  24973  fundmpss  25382  predel  25450  sltres  25611  funpartfun  25780  axcontlem2  25896  axcontlem7  25901  axcontlem8  25902  axcontlem10  25904  outsideofcol  26059  itg2addnc  26249  itg2gt0cn  26250  ftc1anclem3  26272  fnebas  26344  filnetlem3  26400  istotbnd3  26471  totbndmet  26472  sstotbnd2  26474  sstotbnd  26475  equivtotbnd  26478  bndmet  26481  totbndbnd  26489  prdstotbnd  26494  crngorngo  26601  prrngorngo  26652  divrngpr  26654  an3  26688  nacsacs  26754  eldiophelnn0  26813  jm2.17a  27016  jm2.17b  27017  jm2.17c  27018  jm2.27c  27069  jm3.1lem1  27079  jm3.1lem2  27080  jm3.1lem3  27081  lnmlmod  27145  lbslinds  27271  lnrrng  27284  mncply  27310  psgneu  27397  idomrootle  27479  idomodle  27480  hashgcdlem  27484  stoweidlem14  27730  stoweidlem16  27732  stoweidlem24  27740  stoweidlem39  27755  stoweidlem50  27766  stoweidlem51  27767  stoweidlem54  27770  stoweidlem57  27773  wallispilem3  27783  ndmafv  27971  frgrawopreg  28375  2uasbanh  28585  bnj563  29048  bnj658  29056  bnj667  29057  bnj570  29213  bnj938  29245  bnj1001  29266  bnj1006  29267  bnj1049  29280  bnj1121  29291  bnj1173  29308  bnj1177  29312  bnj1245  29320  bnj1311  29330  bnj1321  29333  bnj1388  29339  bnj1398  29340  bnj1415  29344  bnj1417  29347  bnj1421  29348  bnj1442  29355  bnj1452  29358  bnj1489  29362  bnj1312  29364  ollat  29948  omlol  29975  cvlatl  30060  hlomcmcv  30091  2dim  30204  1dimN  30205  lcfl8b  32239  lclkrlem2  32267  lclkrslem1  32272  lclkrslem2  32273  lcfrlem9  32285  mapdval2N  32365  mapdordlem2  32372  mapdrvallem2  32380
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