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

Theorem simplbi 448
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 188 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simpld 447 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  3simpa  955  sbequ2  1661  reurex  2928  eqimss  3386  pssss  3428  eldifi  3455  inss1  3546  ssunsn2  3982  pwssun  4518  sopo  4549  wefr  4601  ordtr  4624  opelxp1  4940  relop  5052  funmo  5499  funrel  5500  fnfun  5571  ffn  5620  f1f  5668  f1of1  5702  f1ofo  5710  isof1o  6074  eqopi  6412  1st2nd2  6415  reldmtpos  6516  swoer  6962  erdisj  6981  ecopover  7037  sdomdom  7164  inf3lemd  7611  mapfien  7682  cardprclem  7897  infxpenlem  7926  cardinfima  8009  dfac5lem4  8038  domtriomlem  8353  smobeth  8492  fpwwe2lem6  8541  fpwwe2lem7  8542  fpwwe2lem12  8547  fpwwe2lem13  8548  fpwwe2  8549  axrnegex  9068  axpre-sup  9075  zre  10317  nnssz  10332  ixxss1  10965  ixxss2  10966  ixxss12  10967  lbioo  10978  ubioo  10979  iccss2  11012  elfzuz  11086  uzdisj  11150  splfv1  11815  sqrlem6  12084  rlimf  12326  lo1f  12343  lo1dm  12344  o1f  12354  o1dm  12355  fsumge0  12605  mertenslem2  12693  divalglem9  12952  bitsinv2  12986  bitsf1ocnv  12987  gcdcllem1  13042  prmnn  13113  prmind2  13121  nprm  13124  prmuz2  13128  isprm6  13140  exprmfct  13141  isprm5  13143  maxprmfct  13144  phibndlem  13190  phibnd  13191  dfphi2  13194  phimullem  13199  pclem  13243  pcprendvds2  13246  pcpre1  13247  expnprm  13302  prmreclem1  13315  1arith  13326  4sqlem15  13358  4sqlem16  13359  vdwlem5  13384  vdwlem6  13385  vdwlem8  13387  vdwlem9  13388  vdwlem11  13390  ramtlecl  13399  0ramcl  13422  firest  13691  acsmre  13908  posprs  14437  latpos  14509  dlatl  14652  pslem  14669  tsrlemax  14683  tsrps  14684  laps  14699  mndlem1  14725  grpmnd  14848  nsgsubg  15003  ghmgrp1  15039  ghmgrp2  15040  gimghm  15082  gagrp  15100  gaset  15101  efgredeu  15415  ablgrp  15448  cmnmnd  15458  cyggenod2  15526  cyggrp  15530  ablfac2  15678  crngrng  15705  dvdsrcl  15785  unitcl  15795  drngrng  15873  subrgrng  15902  subrgrcl  15904  srngrhm  15970  lmimlmhm  16167  lveclmod  16209  2idlcpbl  16336  divs1  16337  divsrhm  16339  lpirrng  16354  nzrrng  16363  domnnzr  16386  fldidom  16396  assalmod  16410  assarng  16411  assasca  16412  cygznlem1  16878  cygznlem3  16881  topontop  17022  tpstop  17035  clsval2  17145  mretopd  17187  neiptoptop  17226  perftop  17251  restfpw  17274  cntop1  17335  cntop2  17336  cnptop1  17337  cnptop2  17338  cnprcl  17340  t1ficld  17422  t0top  17424  t1top  17425  haustop  17426  regtop  17428  nrmtop  17431  cnrmtop  17432  pnrmnrm  17435  cmptop  17489  discmp  17492  tgcmp  17495  uncmp  17497  conndisj  17510  contop  17511  1stctop  17537  llytop  17566  nllytop  17567  hmeocn  17823  filfbas  17911  ufilfil  17967  flimtop  18028  flimfil  18032  alexsublem  18106  ptcmplem3  18116  tsmsfbas  18188  tsmslem1  18189  tsmsgsum  18199  tsmssubm  18203  tsmsres  18204  tsmsf1o  18205  tsmsmhm  18206  tsmsadd  18207  tsmsxplem1  18213  tsmsxplem2  18214  tsmsxp  18215  tlmtmd  18247  tlmlmod  18249  tlmtrg  18250  tvctlm  18257  ressust  18325  uspreg  18335  ucncn  18346  neipcfilu  18357  cuspusp  18361  isxmet2d  18388  metxmet  18395  xmstps  18514  msxms  18515  xmsxmet  18517  msmet  18518  stdbdxmet  18576  nrgngp  18729  nlmngp  18744  nlmlmod  18745  nlmnrg  18746  nvcnlm  18762  nmoi  18793  nghmrcl1  18797  nghmrcl2  18798  nmhmrcl1  18812  nmhmrcl2  18813  qdensere  18835  xrge0gsumle  18895  xrge0tsms  18896  metds0  18911  metdstri  18912  metdsre  18914  metdseq0  18915  metdscnlem  18916  metnrmlem1a  18919  metnrmlem1  18920  icopnfcnv  18998  icopnfhmeo  18999  cmetmet  19270  cmsms  19332  hlbn  19348  ovolicc1  19443  ovolicc2lem5  19448  mblss  19458  mbff  19548  mbfres  19565  mbfadd  19582  mbfsub  19583  i1fmbf  19596  mbfmul  19647  bddmulibl  19759  limcmpt  19801  c1liplem1  19911  c1lip2  19913  fta1glem1  20119  fta1glem2  20120  fta1g  20121  fta1b  20123  ply1pid  20133  aacn  20265  ulmf2  20331  logdmnrp  20563  logdmss  20564  logcnlem2  20565  logcnlem3  20566  logcnlem4  20567  logcnlem5  20568  logcn  20569  dvloglem  20570  logf1o2  20572  efopnlem1  20578  logtayl2  20584  cxpcn  20660  cxpcn3lem  20662  cxpcn3  20663  resqrcn  20664  atandmneg  20777  atandmcj  20780  cosatan  20792  cosatanne0  20793  birthdaylem1  20821  areacl  20832  cxp2lim  20846  jensenlem2  20857  jensen  20858  wilth  20885  sqff1o  20996  dvdsmulf1o  21010  mersenne  21042  bposlem3  21101  lgsqrlem1  21156  lgsqrlem2  21157  lgsqrlem3  21158  lgsqrlem4  21159  lgseisenlem3  21166  lgsquad2lem2  21174  2sqlem6  21184  chebbnd1  21197  chtppilim  21200  chpchtlim  21204  chpo1ub  21205  rplogsumlem1  21209  rplogsumlem2  21210  dchrmusumlema  21218  dchrvmasumiflem1  21226  dchrisum0flblem2  21234  dchrisum0lema  21239  dchrisum0lem2  21243  selberg3lem2  21283  pntrsumo1  21290  selbergsb  21300  pnt2  21338  ostthlem2  21353  ostth2lem2  21359  uhgra0v  21376  usgra0v  21422  usgra1v  21440  eupagra  21719  ablogrpo  21903  smgrpismgm  21951  mndoissmgrp  21958  nmogtmnf  22302  bnnv  22399  hlobn  22421  hcauseq  22718  hlimseqi  22722  hlimveci  22723  shss  22743  sh0  22749  chsh  22758  lnopf  23393  bdopln  23395  nmopgtmnf  23402  hmopf  23408  lnfnf  23418  unopf1o  23450  elunop2  23547  elpjhmop  23719  stcltrlem1  23810  mdslle1i  23851  mdslle2i  23852  rabexgfGS  24018  ssnnssfz  24179  tospos  24217  xrge0tsmsd  24254  ofldsqr  24271  ofldlt1  24274  ofldchr  24275  lmxrge0  24368  qqhrhm  24404  esumpcvgval  24499  measssd  24600  elmbfmvol2  24648  domprobmeas  24699  ballotlemscr  24807  ballotlemfg  24814  ballotlemfrc  24815  ballotlemfrceq  24817  ballotlemrinv0  24821  subfacval3  24906  pcontop  24943  sconpcon  24945  cvmcn  24980  cvmliftlem10  25012  fundmpss  25421  predel  25489  sltres  25650  funpartfun  25819  axcontlem2  25935  axcontlem7  25940  axcontlem8  25941  axcontlem10  25943  outsideofcol  26098  itg2addnc  26297  itg2gt0cn  26298  ftc1anclem3  26320  fnebas  26391  filnetlem3  26447  istotbnd3  26518  totbndmet  26519  sstotbnd2  26521  sstotbnd  26522  equivtotbnd  26525  bndmet  26528  totbndbnd  26536  prdstotbnd  26541  crngorngo  26648  prrngorngo  26699  divrngpr  26701  an3  26735  nacsacs  26801  eldiophelnn0  26860  jm2.17a  27063  jm2.17b  27064  jm2.17c  27065  jm2.27c  27116  jm3.1lem1  27126  jm3.1lem2  27127  jm3.1lem3  27128  lnmlmod  27192  lbslinds  27318  lnrrng  27331  mncply  27357  psgneu  27444  idomrootle  27526  idomodle  27527  hashgcdlem  27531  stoweidlem14  27777  stoweidlem16  27779  stoweidlem24  27787  stoweidlem39  27802  stoweidlem50  27813  stoweidlem51  27814  stoweidlem54  27817  stoweidlem57  27820  wallispilem3  27830  ndmafv  28018  frgrawopreg  28536  2uasbanh  28746  bnj563  29209  bnj658  29217  bnj667  29218  bnj570  29374  bnj938  29406  bnj1001  29427  bnj1006  29428  bnj1049  29441  bnj1121  29452  bnj1173  29469  bnj1177  29473  bnj1245  29481  bnj1311  29491  bnj1321  29494  bnj1388  29500  bnj1398  29501  bnj1415  29505  bnj1417  29508  bnj1421  29509  bnj1442  29516  bnj1452  29519  bnj1489  29523  bnj1312  29525  ollat  30109  omlol  30136  cvlatl  30221  hlomcmcv  30252  2dim  30365  1dimN  30366  lcfl8b  32400  lclkrlem2  32428  lclkrslem1  32433  lclkrslem2  32434  lcfrlem9  32446  mapdval2N  32526  mapdordlem2  32533  mapdrvallem2  32541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator